src/ZF/ex/Primrec.ML
1999-01-29 paulson 1999-01-29 expandshort
1999-01-27 paulson 1999-01-27 automatic insertion of datatype intr rules into claset
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1999-01-13 paulson 1999-01-13 datatype package improvements
1999-01-08 paulson 1999-01-08 removal of DO_GOAL
1999-01-07 paulson 1999-01-07 ZF: the natural numbers as a datatype
1999-01-06 paulson 1999-01-06 induct_tac and exhaust_tac
1998-12-28 paulson 1998-12-28 Needs separate theory Primrec_defs due to new inductive defs package
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-13 paulson 1998-07-13 Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-26 paulson 1997-05-26 Slight simplifications
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-01-30 clasohm 1996-01-30 expanded tabs
1994-12-14 clasohm 1994-12-14 added bind_thm for theorems defined by "standard ..."
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections