src/FOL/cladata.ML
2000-07-30 wenzelm 2000-07-30 updated ObtainFun;
2000-06-28 paulson 2000-06-28 declaring and using cla_make_elim
2000-01-05 wenzelm 2000-01-05 ObtainFun;
1999-08-25 wenzelm 1999-08-25 proper bootstrap of IFOL/FOL theories and packages;
1999-08-02 wenzelm 1999-08-02 fixed Blast_Data;
1998-11-18 wenzelm 1998-11-18 blast: cla_method';
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 paulson 1997-11-26 The change from iffE to iffCE means fewer case splits in most cases. Very few proofs are affected, almost none adversely
1997-11-03 wenzelm 1997-11-03 adapted to new implicit claset;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-06 berghofe 1997-08-06 Moved functions from file "thy_data.ML".
1997-04-02 paulson 1997-04-02 Now builds blast_tac
1997-03-27 paulson 1997-03-27 Now uses the alternative (safe!) rules for ex1
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF