src/HOL/ex/Classical.thy
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-29 wenzelm 2009-07-29 Meson.first_order_resolve: avoid handle _; proper context for various Meson and Metis rules and tactics unified meson_tac/meson_claset_tac;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-06-26 paulson 2007-06-26 updated for metis method
2007-04-19 paulson 2007-04-19 trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions
2007-01-09 paulson 2007-01-09 simplified the resoution proofs
2007-01-04 paulson 2007-01-04 improvements to proof reconstruction. Some files loaded in a different order
2006-12-22 paulson 2006-12-22 revised for new make_clauses
2006-10-23 paulson 2006-10-23 new single-step proofs
2006-10-20 paulson 2006-10-20 example of a single-step proof reconstruction
2005-12-14 paulson 2005-12-14 modified example for new clauses
2005-06-28 paulson 2005-06-28 stylistic improvements
2005-06-24 paulson 2005-06-24 meson method taking an argument list
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-20 paulson 2005-05-20 converted some problems to Isar format
2004-12-07 paulson 2004-12-07 renamed attributes to lower case
2004-08-20 paulson 2004-08-20 proof reconstruction for external ATPs
2004-08-06 paulson 2004-08-06 modified resolution proof
2004-06-28 paulson 2004-06-28 new method for explicit classical resolution
2003-10-29 paulson 2003-10-29 tidying
2003-10-08 paulson 2003-10-08 Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy