src/HOL/Decision_Procs/MIR.thy
Fri, 05 Aug 2016 15:44:53 +0200 nipkow fixed floor proof
Wed, 17 Feb 2016 21:51:55 +0100 haftmann consolidated name
Mon, 28 Dec 2015 01:28:28 +0100 wenzelm more symbols;
Sun, 27 Dec 2015 21:46:36 +0100 wenzelm prefer symbols for "floor", "ceiling";
Tue, 01 Dec 2015 14:09:10 +0000 paulson Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
Tue, 17 Nov 2015 12:32:08 +0000 paulson Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
Fri, 13 Nov 2015 15:59:40 +0000 paulson MIR decision procedure again working
Fri, 13 Nov 2015 12:27:13 +0000 paulson Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
Tue, 10 Nov 2015 14:43:29 +0000 paulson Merge
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Thu, 05 Nov 2015 10:39:59 +0100 wenzelm isabelle update_cartouches -c -t;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Tue, 01 Sep 2015 22:32:58 +0200 wenzelm eliminated \<Colon>;
Sat, 20 Jun 2015 16:31:44 +0200 wenzelm isabelle update_cartouches;
Mon, 01 Jun 2015 11:46:03 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 05 Nov 2014 22:37:14 +0100 wenzelm more symbols;
Sun, 21 Sep 2014 16:56:11 +0200 haftmann explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Tue, 09 Sep 2014 20:51:36 +0200 blanchet ported Decision_Procs to new datatypes
Tue, 09 Sep 2014 20:51:36 +0200 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
Thu, 07 Aug 2014 12:17:41 +0200 blanchet no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Wed, 11 Jun 2014 14:24:23 +1000 Thomas Sewell Hypsubst preserves equality hypotheses
Sat, 12 Apr 2014 17:26:27 +0200 nipkow made mult_pos_pos a simp rule
Wed, 09 Apr 2014 09:37:47 +0200 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
Fri, 04 Apr 2014 17:58:25 +0100 paulson divide_minus_left divide_minus_right are in field_simps but are not default simprules
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Wed, 19 Feb 2014 16:32:37 +0100 blanchet merged 'List.set' with BNF-generated 'set'
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Fri, 23 Aug 2013 17:01:12 +0200 wenzelm tuned signature;
Thu, 07 Mar 2013 17:50:26 +0100 wenzelm tuned proofs -- more structure, less warnings;
Mon, 25 Feb 2013 12:17:50 +0100 wenzelm prefer stateless 'ML_val' for tests;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Wed, 28 Nov 2012 15:59:18 +0100 wenzelm eliminated slightly odd identifiers;
Tue, 27 Nov 2012 13:22:29 +0100 wenzelm eliminated some improper identifiers;
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Mon, 03 Sep 2012 09:15:40 +0200 wenzelm some parallel ML;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Tue, 27 Mar 2012 14:49:56 +0200 huffman remove redundant lemmas
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Sat, 25 Feb 2012 09:07:39 +0100 bulwahn removing unnecessary assumptions in RealDef;
Fri, 06 Jan 2012 10:19:48 +0100 haftmann prefer concat over foldl append []
Fri, 02 Dec 2011 14:54:25 +0100 wenzelm more antiquotations;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Thu, 03 Mar 2011 21:43:06 +0100 wenzelm tuned proofs -- eliminated prems;
Thu, 03 Mar 2011 15:19:20 +0100 wenzelm removed spurious 'unused_thms' (cf. 1a65b780bd56);
Fri, 25 Feb 2011 20:07:48 +0100 nipkow Some cleaning up
Thu, 24 Feb 2011 21:54:28 +0100 krauss recdef -> fun(ction)
Thu, 24 Feb 2011 17:38:05 +0100 krauss eliminated clones of List.upto
Mon, 21 Feb 2011 23:47:19 +0100 wenzelm tuned proofs -- eliminated prems;
Fri, 07 Jan 2011 18:10:42 +0100 bulwahn adopting proofs due to new list comprehension to set comprehension simproc
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Fri, 27 Aug 2010 10:56:46 +0200 haftmann formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
less more (0) -60 tip