aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa/example.ML
Commit message (Expand)AuthorAge
* Cleaned up example files so all demonstrate same theorem "conj_comms".Gravatar David Aspinall1999-09-13
* tuned;Gravatar Makarius Wenzel1999-08-06
* Fix for splash hack for theory files when proo-splash-inhibit=t.Gravatar David Aspinall1998-12-10
* Fixes to debug long standing not-showing-first-goal problem.Gravatar David Aspinall1998-11-25
* Removed duplicate proofGravatar David Aspinall1998-10-20
* Added Id to headers.Gravatar David Aspinall1998-09-09
* More features working. Added example.Gravatar David Aspinall1998-09-08
* Added Isabelle example and skeleton for Coq and Lego.Gravatar David Aspinall1998-09-03