aboutsummaryrefslogtreecommitdiff
path: root/isar/Example.thy
AgeCommit message (Expand)Author
2003-02-18Decoration to show off MMM modeDavid Aspinall
2002-09-11Remove comment about selecting PG/Isar.David Aspinall
2002-08-12Remove comment at the end testing feature. See etc/isar/Parsing.thy instead.David Aspinall
2002-01-16WhitespaceDavid Aspinall
2001-12-27tuned;Makarius Wenzel
2001-09-04tuned proof text;Makarius Wenzel
2000-06-22Extra note.David Aspinall
2000-06-08proper indentation;Makarius Wenzel
2000-06-01Removed now spurious semicolons, 8-).David Aspinall
2000-05-29Add -*- isar -*- tag to force mode, and comment to explain.David Aspinall
1999-09-24tuned;Makarius Wenzel
1999-09-24unified example with other proof assistants;Makarius Wenzel
1999-09-21lemma and_comms;Makarius Wenzel
1999-08-18tuned;Makarius Wenzel
1999-05-27oops;Makarius Wenzel
1999-05-27be chatty;Makarius Wenzel
1999-05-25more examples;Makarius Wenzel
1999-04-16initial version of 'isar proof assistant (Isabelle/Isar);Makarius Wenzel