src/HOL/Hoare/hoare_tac.ML
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 06 Sep 2015 22:14:51 +0200 haftmann prefer "uncurry" as canonical name for case distinction on products in combinatorial view
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Fri, 21 Feb 2014 20:47:48 +0100 wenzelm tuned whitespace;
Fri, 21 Feb 2014 20:37:13 +0100 wenzelm proper ML structure with signature;
Fri, 21 Feb 2014 20:29:33 +0100 wenzelm reduced ML warnings;
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 17 Aug 2011 18:05:31 +0200 wenzelm modernized signature of Term.absfree/absdummy;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Fri, 07 Jan 2011 18:32:19 +0100 wenzelm do not open ML structures;
Tue, 27 Jul 2010 17:09:35 +0200 haftmann delete structure Basic_Record; avoid `record` in names in structure Record
Thu, 01 Jul 2010 16:54:42 +0200 haftmann qualified constants Set.member and Set.Collect
Mon, 28 Jun 2010 15:03:07 +0200 haftmann merged constants "split" and "prod_case"
Thu, 10 Jun 2010 12:24:03 +0200 haftmann tuned quotes, antiquotations and whitespace
Wed, 26 May 2010 16:28:55 +0200 haftmann dropped legacy theorem bindings
Wed, 26 May 2010 16:05:25 +0200 haftmann normalized references to constant "split"
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Thu, 23 Jul 2009 18:44:09 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
Thu, 02 Oct 2008 14:22:36 +0200 wenzelm major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Mon, 16 Jun 2008 22:13:52 +0200 wenzelm renamed rename_params_tac to rename_tac;
Mon, 17 Mar 2008 18:37:00 +0100 wenzelm removed duplicate lemmas;
Wed, 29 Aug 2007 16:46:08 +0200 wenzelm added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
less more (0) tip