19960216 
paulson 
19960216 
Elimination of fullyfunctorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

file  diff  annotate 
19960130 
clasohm 
19960130 
expanded tabs

file  diff  annotate 
19951121 
clasohm 
19951121 
main directory is now read by exit_use_dir, too;
removed make_chart from ROOT.ML

file  diff  annotate 
19951024 
clasohm 
19951024 
added calls of init_html and make_chart

file  diff  annotate 
19950425 
lcp 
19950425 
Now loads the theory "Let". Could add it to FOL, but this appears to
be incompatible with CCL.

file  diff  annotate 
19941216 
lcp 
19941216 
changed useless "qed" calls for lemmas back to uses of "result",
and/or used "bind_thm" to declare the real results.

file  diff  annotate 
19940825 
lcp 
19940825 
ZF/Inductive.thy,.ML: renamed from "inductive" to allow rebuilding 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

file  diff  annotate 
19940816 
lcp 
19940816 
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass

file  diff  annotate 
19940812 
lcp 
19940812 
installation of new inductive/datatype sections

file  diff  annotate 
19940727 
lcp 
19940727 
Addition of infinite branching datatypes

file  diff  annotate 
19940726 
lcp 
19940726 
Axiom of choice, cardinality results, etc.

file  diff  annotate 
19940621 
lcp 
19940621 
Addition of cardinals and order types, various tidying

file  diff  annotate 
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 