1993-11-18 lcp [Thu, 18 Nov 1993 14:57:05 +0100] rev 127
Misc modifs such as expandshort
src/ZF/Arith.ML src/ZF/arith.ML

1993-11-16 clasohm [Tue, 16 Nov 1993 19:50:20 +0100] rev 126
added loaded_thys to signature and removed list_/set_loaded

1993-11-16 clasohm [Tue, 16 Nov 1993 14:26:15 +0100] rev 125
changed use_thy's parameter to exact theory name

1993-11-16 clasohm [Tue, 16 Nov 1993 14:24:21 +0100] rev 124
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
src/ZF/Arith.thy src/ZF/Bool.thy src/ZF/Datatype.thy src/ZF/Epsilon.thy src/ZF/Fixedpt.thy src/ZF/List.ML src/ZF/List.thy src/ZF/ListFn.thy src/ZF/Nat.thy src/ZF/Ord.thy src/ZF/Pair.thy src/ZF/Perm.thy src/ZF/QPair.thy src/ZF/QUniv.thy src/ZF/ROOT.ML src/ZF/Sum.thy src/ZF/Trancl.thy src/ZF/Univ.thy src/ZF/WF.thy src/ZF/arith.thy src/ZF/bool.thy src/ZF/coinductive.thy src/ZF/constructor.thy src/ZF/datatype.thy src/ZF/domrange.thy src/ZF/epsilon.thy src/ZF/equalities.thy src/ZF/fin.ML src/ZF/fin.thy src/ZF/fixedpt.thy src/ZF/func.thy src/ZF/ind_syntax.thy src/ZF/indrule.thy src/ZF/inductive.thy src/ZF/intr_elim.thy src/ZF/list.ML src/ZF/list.thy src/ZF/listfn.thy src/ZF/mono.thy src/ZF/nat.thy src/ZF/ord.thy src/ZF/pair.thy src/ZF/perm.thy src/ZF/qpair.thy src/ZF/quniv.thy src/ZF/simpdata.thy src/ZF/subset.thy src/ZF/sum.thy src/ZF/trancl.thy src/ZF/univ.thy ...

1993-11-16 clasohm [Tue, 16 Nov 1993 14:23:19 +0100] rev 123
moved call of store_theory to end of use t.thy; use t.ML;
use_thy now needs the exact theory name (capital/lower letters);
improved handling of incompletly read theories;
added function unlink_thy, removed function relations;
added reference variable delete_tmpfile;
removed some bugs
src/Pure/Thy/read.ML src/Pure/Thy/syntax.ML

1993-11-16 clasohm [Tue, 16 Nov 1993 14:13:11 +0100] rev 122
replaced \un by \union in "Simplification sets"

1993-11-16 clasohm [Tue, 16 Nov 1993 14:10:19 +0100] rev 121
changed use_thy's parameter to exact theory name

1993-11-15 lcp [Mon, 15 Nov 1993 14:41:25 +0100] rev 120
changed all co- and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs
src/ZF/Datatype.ML src/ZF/Nat.ML src/ZF/QPair.thy src/ZF/QUniv.ML src/ZF/ROOT.ML src/ZF/ZF.ML src/ZF/coinductive.ML src/ZF/datatype.ML src/ZF/ex/BinFn.ML src/ZF/ex/LList.ML src/ZF/ex/LListFn.ML src/ZF/ex/LListFn.thy src/ZF/ex/LList_Eq.ML src/ZF/ex/ROOT.ML src/ZF/ex/binfn.ML src/ZF/ex/counit.ML src/ZF/ex/llist.ML src/ZF/ex/llist_eq.ML src/ZF/ex/llistfn.ML src/ZF/ex/llistfn.thy src/ZF/nat.ML src/ZF/qpair.thy src/ZF/quniv.ML src/ZF/zf.ML

1993-11-15 lcp [Mon, 15 Nov 1993 14:33:40 +0100] rev 119
boolE: changed to have equality assumptions instead of P(c); proved many boolean laws
src/ZF/Bool.ML src/ZF/bool.ML

1993-11-15 lcp [Mon, 15 Nov 1993 12:58:21 +0100] rev 118
Added commentary