Tue, 06 Sep 1994 14:44:10 +0200 renamed base_on into mk_base and moved it to the beginning of the generated
clasohm [Tue, 06 Sep 1994 14:44:10 +0200] rev 586
renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
Tue, 06 Sep 1994 13:46:53 +0200 Pure/type/unvarifyT: moved there from logic.ML
lcp [Tue, 06 Sep 1994 13:46:53 +0200] rev 585
Pure/type/unvarifyT: moved there from logic.ML
Tue, 06 Sep 1994 13:28:56 +0200 documentation of theory sections (co)inductive and (co)datatype
lcp [Tue, 06 Sep 1994 13:28:56 +0200] rev 584
documentation of theory sections (co)inductive and (co)datatype
Tue, 06 Sep 1994 13:10:38 +0200 minor internal changes;
wenzelm [Tue, 06 Sep 1994 13:10:38 +0200] rev 583
minor internal changes;
Tue, 06 Sep 1994 13:09:58 +0200 added ext_tsig_types;
wenzelm [Tue, 06 Sep 1994 13:09:58 +0200] rev 582
added ext_tsig_types; various minor changes;
Tue, 06 Sep 1994 11:02:16 +0200 removal of needless quotes
lcp [Tue, 06 Sep 1994 11:02:16 +0200] rev 581
removal of needless quotes
Wed, 31 Aug 1994 17:34:12 +0200 Updated datatype documentation with a few hints
nipkow [Wed, 31 Aug 1994 17:34:12 +0200] rev 580
Updated datatype documentation with a few hints
Thu, 25 Aug 1994 12:21:00 +0200 new file of useful things for writing theory sections
lcp [Thu, 25 Aug 1994 12:21:00 +0200] rev 579
new file of useful things for writing theory sections
Thu, 25 Aug 1994 12:09:21 +0200 ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp [Thu, 25 Aug 1994 12:09:21 +0200] rev 578
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without the keyword "inductive" making the theory file fail ZF/Makefile: now has Inductive.thy,.ML ZF/Datatype,Finite,Zorn: depend upon Inductive ZF/intr_elim: now checks that the inductive name does not clash with existing theory names ZF/ind_section: deleted things replicated in Pure/section_utils.ML ZF/ROOT: now loads Pure/section_utils
Thu, 25 Aug 1994 10:41:17 +0200 print_sign_exn: now exported, with a polymorphic type
lcp [Thu, 25 Aug 1994 10:41:17 +0200] rev 577
print_sign_exn: now exported, with a polymorphic type
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip