2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-07-08 wenzelm 2015-07-08 Variable.focus etc.: optional bindings provided by user; Subgoal.focus command: more careful treatment of user-provided bindings;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
2013-11-23 wenzelm 2013-11-23 more accurate goal context; actually check assertions;
2012-02-27 wenzelm 2012-02-27 prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
2011-10-18 huffman 2011-10-18 hide typedef-generated constants and Sum_Type.sum
2011-07-25 blanchet 2011-07-25 make compile
2010-08-30 haftmann 2010-08-30 what is hidden is hidden
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
2010-07-12 wenzelm 2010-07-12 some modernization of really ancient Meson experiments;
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-06-11 haftmann 2010-06-11 hide sum explicitly
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns
2010-05-13 ballarin 2010-05-13 Fix syntax; apparently constant apply was introduced in an earlier changeset.
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
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-07-24 wenzelm 2009-07-24 do not open OldGoals;
2009-07-24 wenzelm 2009-07-24 explicit OldGoals;
2009-07-22 haftmann 2009-07-22 set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality
2008-02-06 chaieb 2008-02-06 between constant removed
2008-01-21 berghofe 2008-01-21 Removed Logic.auto_rename.
2007-08-20 haftmann 2007-08-20 turned locales intro classes
2007-08-17 wenzelm 2007-08-17 proper signature for Meson;
2007-08-02 wenzelm 2007-08-02 reset Logic.auto_rename;
2007-08-02 wenzelm 2007-08-02 tuned;
2007-08-02 wenzelm 2007-08-02 converted Meson tests to proper theory;