src/FOL/fologic.ML
11 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
2011-08-17 wenzelm 2011-08-17 modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-08-17 haftmann 2010-08-17 more antiquotations
2009-08-29 wenzelm 2009-08-29 eliminated hard tabs;
2009-07-09 wenzelm 2009-07-09 removed obsolete CVS Ids;
2008-06-23 wenzelm 2008-06-23 removed obsolete dest_concls;
2001-10-04 wenzelm 2001-10-04 added dest_conj, dest_concls;
2000-11-03 wenzelm 2000-11-03 removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
2000-09-05 wenzelm 2000-09-05 added not;
2000-08-07 paulson 2000-08-07 new abstract syntax operations, used in ZF
2000-07-30 wenzelm 2000-07-30 added atomic_Trueprop;
1999-10-04 wenzelm 1999-10-04 added mk_conj, mk_disj, mk_imp;
1999-01-19 paulson 1999-01-19 tidied; added dest_eq
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-12-03 paulson 1997-12-03 Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic