19931118 
lcp 
19931118 
Misc modifs such as expandshort

file  diff  annotate 
19931005 
lcp 
19931005 
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
changes
epsilon,arith: many changes
ordinal/succ_mem_succI/E: deleted; use succ_leI/E
nat/nat_0_in_succ: deleted; use nat_0_le
univ/Vset_rankI: deleted; use VsetI

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 
19930916 
clasohm 
19930916 
Initial revision

file  diff  annotate 