src/ZF/UNITY/Constrains.thy
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-03-06 paulson 2012-03-06 More mathematical symbols for ZF examples
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2010-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-07-29 wenzelm 2007-07-29 replaced program_defs_ref by proper context data (via attribute "program");
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-07-03 wenzelm 2007-07-03 rewrite_goal_tac;
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2005-06-02 paulson 2005-06-02 renamed "constrains" to "safety" to avoid keyword clash
2005-03-28 paulson 2005-03-28 conversion of UNITY to Isar scripts
2003-05-27 paulson 2003-05-27 updating ZF-UNITY with Sidi's new material
2001-11-15 ehmety 2001-11-15 *** empty log message ***
2001-08-08 paulson 2001-08-08 new ZF/UNITY theory