Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/HOL/ex/Meson_Test.thy
2015-08-16 wenzelm 2015-08-16 added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf); file | diff | annotate
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context; file | diff | annotate
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; file | diff | annotate
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context); file | diff | annotate
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section; file | diff | annotate
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; file | diff | annotate
2013-11-23 wenzelm 2013-11-23 more accurate goal context; actually check assertions; file | diff | annotate
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; file | diff | annotate
2011-10-18 huffman 2011-10-18 hide typedef-generated constants Product_Type.prod and Sum_Type.sum file | diff | annotate
2011-07-25 blanchet 2011-07-25 make compile file | diff | annotate
2010-08-30 haftmann 2010-08-30 what is hidden is hidden file | diff | annotate
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq file | diff | annotate
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies file | diff | annotate
2010-07-12 wenzelm 2010-07-12 some modernization of really ancient Meson experiments; file | diff | annotate
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy file | diff | annotate
2010-06-11 haftmann 2010-06-11 hide sum explicitly file | diff | annotate
2010-05-26 boehmes 2010-05-26 hide constants and types introduced by SMT, simplified SMT patterns syntax, added examples for SMT patterns file | diff | annotate
2010-05-13 ballarin 2010-05-13 Fix syntax; apparently constant apply was introduced in an earlier changeset. file | diff | annotate
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; file | diff | annotate
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; file | diff | annotate
2009-07-24 wenzelm 2009-07-24 do not open OldGoals; file | diff | annotate
2009-07-24 wenzelm 2009-07-24 explicit OldGoals; file | diff | annotate
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 file | diff | annotate
2008-04-22 haftmann 2008-04-22 constant HOL.eq now qualified file | diff | annotate
2008-04-02 haftmann 2008-04-02 explicit class "eq" for operational equality file | diff | annotate
2008-02-06 chaieb 2008-02-06 between constant removed file | diff | annotate
2008-01-21 berghofe 2008-01-21 Removed Logic.auto_rename. file | diff | annotate
2007-08-20 haftmann 2007-08-20 turned locales intro classes file | diff | annotate
2007-08-17 wenzelm 2007-08-17 proper signature for Meson; file | diff | annotate
2007-08-02 wenzelm 2007-08-02 reset Logic.auto_rename; file | diff | annotate
2007-08-02 wenzelm 2007-08-02 tuned; file | diff | annotate
2007-08-02 wenzelm 2007-08-02 converted Meson tests to proper theory; file | diff | annotate
isabelle