19940506 
lcp 
19940506 
renaming/removal of filenames to correct case

file  diff  annotate 
19931116 
clasohm 
19931116 
made pseudo theories for all ML files;
documented dependencies between all thy and ML files

file  diff  annotate 
19931115 
lcp 
19931115 
changed all co and co_ to co
ZF/ex/llistfn: new coinduction example: flip
ZF/ex/llist_eq: now uses standard pairs not qpairs

file  diff  annotate 
19931104 
clasohm 
19931104 
renamed some files

file  diff  annotate 
19931022 
clasohm 
19931022 
added h 15000 for Poly/ML in Makefile,
changed ROOT.ML for new Readthy

file  diff  annotate 
19931011 
clasohm 
19931011 
renamed ordinal.* to ord.*

file  diff  annotate 
19931006 
clasohm 
19931006 
changed "listfn" to "listfn"

file  diff  annotate 
19930930 
lcp 
19930930 
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
domrange/image_subset,vimage_subset: deleted needless premise!
misc: This slightly simplifies two proofs in SchroederBernstein Theorem
indsyntax/rule_concl: recoded to avoid exceptions
intrelim: now checks conclusions of introduction rules
func/fun_disjoint_Un: now uses ex_ex1I
listfn/hd,tl,drop: new
simpdata/bquant_simps: new
list/list_case_type: restored!
bool.thy: changed 1 from a "def" to a translation
Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML
nat/succ_less_induct: new induction principle
arith/add_mono: new results about monotonicity
simpdata/mem_simps: removed the ones for succ and cons; added succI1,
consI2 to ZF_ss
upair/succ_iff: new, for use with simp_tac (cons_iff already existed)
ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ
nat/nat_0_in_succ: new
ex/proplog/hyps_thms_if: split up the fast_tac call for more speed

file  diff  annotate 
19930917 
lcp 
19930917 
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.

file  diff  annotate 
19930917 
lcp 
19930917 
test commit

file  diff  annotate 
19930916 
clasohm 
19930916 
Initial revision

file  diff  annotate 