19990921 
nipkow 
19990921 
Mod because of new solver interface.

file  diff  annotate 
19990127 
paulson 
19990127 
new typechecking solver for the simplifier

file  diff  annotate 
19980924 
oheimb 
19980924 
renamed mk_meta_eq to mk_eq

file  diff  annotate 
19980817 
paulson 
19980817 
Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
contains fewer theorems than before

file  diff  annotate 
19980727 
paulson 
19980727 
A few new lemmas by Mark Staples

file  diff  annotate 
19980713 
paulson 
19980713 
Huge tidyup: removal of leading \!\!
addsplits split_tac[split_if] now default
nat_succI now included by default

file  diff  annotate 
19971103 
wenzelm 
19971103 
isatool fixclasimp;

file  diff  annotate 
19971014 
nipkow 
19971014 
Added neagtion rules for Ball and Bex.
ZF/AC now fails to build. Larry to fix.

file  diff  annotate 
19971010 
wenzelm 
19971010 
fixed dots;

file  diff  annotate 
19970606 
paulson 
19970606 
Better miniscoping for bounded quantifiers

file  diff  annotate 
19970402 
paulson 
19970402 
Uses ZF.thy again, to make that theory usable

file  diff  annotate 
19970109 
paulson 
19970109 
Removal of needless "addIs [equality]", etc.

file  diff  annotate 
19970107 
paulson 
19970107 
Default rewrite rules for quantification over Collect(A,P)

file  diff  annotate 
19970103 
paulson 
19970103 
Implicit simpsets and clasets for FOL and ZF

file  diff  annotate 
19960607 
paulson 
19960607 
Addition of converse_iff, domain_converse, range_converse as rewrites

file  diff  annotate 
19960326 
paulson 
19960326 
Added new rewrite rules about cons and succ

file  diff  annotate 
19960130 
clasohm 
19960130 
expanded tabs

file  diff  annotate 
19950413 
lcp 
19950413 
Recoded function atomize so that new ways of creating
simplification rules can be added easily.

file  diff  annotate 
19950112 
lcp 
19950112 
Added singleton_iff, Sigma_empty1, Sigma_empty2, Collect_simps
and UnInt_simps to ZF_ss. Added consI1 to ZF_typechecks.

file  diff  annotate 
19941208 
lcp 
19941208 
test_assume_tac: now tries eq_assume_tac on exceptional cases
(formulae not of the form a:?A). Affects typechk_tac.

file  diff  annotate 
19940816 
lcp 
19940816 
ZF/pair.ML: moved some definitions here from simpdata.ML

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

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

file  diff  annotate 
19940712 
lcp 
19940712 
new cardinal arithmetic developments

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

file  diff  annotate 
19940317 
lcp 
19940317 
Improved layout for inductive defs

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 