Thu, 09 Oct 2003 18:13:32 +0200 Added support for making constants final, that is, ensuring that no
skalberg [Thu, 09 Oct 2003 18:13:32 +0200] rev 14223
Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
Wed, 08 Oct 2003 16:02:54 +0200 Added axiomatic specifications (ax_specification).
skalberg [Wed, 08 Oct 2003 16:02:54 +0200] rev 14222
Added axiomatic specifications (ax_specification).
Wed, 08 Oct 2003 15:58:15 +0200 now accepts DOS and Mac line breaks
paulson [Wed, 08 Oct 2003 15:58:15 +0200] rev 14221
now accepts DOS and Mac line breaks
Wed, 08 Oct 2003 15:57:41 +0200 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
paulson [Wed, 08 Oct 2003 15:57:41 +0200] rev 14220
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
Fri, 03 Oct 2003 12:36:16 +0200 added a comment
paulson [Fri, 03 Oct 2003 12:36:16 +0200] rev 14219
added a comment
Thu, 02 Oct 2003 10:57:04 +0200 removal of junk and improvement of the document
paulson [Thu, 02 Oct 2003 10:57:04 +0200] rev 14218
removal of junk and improvement of the document
Wed, 01 Oct 2003 11:02:36 +0200 Fixed inefficiency in post_definition by adding weak case congruence
berghofe [Wed, 01 Oct 2003 11:02:36 +0200] rev 14217
Fixed inefficiency in post_definition by adding weak case congruence rules to simpset.
Tue, 30 Sep 2003 17:05:50 +0200 Removed garbage accidentally left behind in file.
ballarin [Tue, 30 Sep 2003 17:05:50 +0200] rev 14216
Removed garbage accidentally left behind in file.
Tue, 30 Sep 2003 15:13:02 +0200 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin [Tue, 30 Sep 2003 15:13:02 +0200] rev 14215
Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
Tue, 30 Sep 2003 15:10:59 +0200 Improvements to Isar/Locales: premises generated by "includes" elements
ballarin [Tue, 30 Sep 2003 15:10:59 +0200] rev 14214
Improvements to Isar/Locales: premises generated by "includes" elements changed.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip