src/HOL/Num.thy
Mon, 17 Jul 2017 16:49:19 +0200 eberlm Printing natural numbers as numerals in evaluation
Sun, 16 Oct 2016 09:31:03 +0200 haftmann de-orphanized declaration
Wed, 12 Oct 2016 21:48:53 +0200 haftmann transfer lifting rule for numeral
Sun, 18 Sep 2016 18:23:59 +0200 Lars Hupel tuned
Wed, 10 Aug 2016 22:05:36 +0200 wenzelm misc tuning and modernization;
Sat, 12 Mar 2016 22:04:52 +0100 haftmann model characters directly as range 0..255
Tue, 01 Mar 2016 10:36:19 +0100 haftmann tuned bootstrap order to provide type classes in a more sensible order
Wed, 17 Feb 2016 21:51:57 +0100 haftmann dropped various legacy fact bindings
Mon, 28 Dec 2015 01:26:34 +0100 wenzelm prefer symbols for "abs";
Mon, 07 Dec 2015 10:38:04 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 09:48:24 +0100 Andreas Lochbihler add various lemmas
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Sat, 18 Jul 2015 22:58:50 +0200 wenzelm isabelle update_cartouches;
Fri, 10 Apr 2015 11:31:10 +0200 wenzelm tuned signature;
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 02 Oct 2014 11:33:06 +0200 haftmann moved lemmas out of Int.thy which have nothing to do with int
Mon, 22 Sep 2014 21:28:57 +0200 wenzelm discontinued old "xnum" token category;
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
Wed, 03 Sep 2014 00:06:26 +0200 blanchet tuned imports
Wed, 03 Sep 2014 00:06:24 +0200 blanchet use 'datatype_new' in 'Main'
Mon, 01 Sep 2014 16:34:40 +0200 blanchet renamed BNF theories
Mon, 01 Sep 2014 16:17:46 +0200 blanchet renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Fri, 07 Mar 2014 11:46:26 +0100 wenzelm more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
Mon, 17 Feb 2014 13:31:42 +0100 blanchet renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Mon, 04 Nov 2013 20:10:06 +0100 haftmann streamlined setup of linear arithmetic
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Sun, 18 Aug 2013 15:29:50 +0200 haftmann generalized sort constraint of lemmas
Sun, 23 Jun 2013 21:16:07 +0200 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
Tue, 28 May 2013 16:29:11 +0200 wenzelm more explicit Printer.type_emphasis, depending on show_type_emphasis;
Mon, 27 May 2013 21:00:30 +0200 wenzelm tuned;
Sat, 25 May 2013 15:37:53 +0200 wenzelm syntax translations always depend on context;
Fri, 15 Feb 2013 08:31:31 +0100 haftmann two target language numeral types: integer and natural, as replacement for code_numeral;
Fri, 11 Jan 2013 08:17:39 +0100 haftmann sharing of recursive results on evaluation
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Wed, 03 Oct 2012 16:59:58 +0200 wenzelm more explicit show_type_constraint, show_sort_constraint;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Mon, 02 Apr 2012 16:07:24 +0200 huffman remove unnecessary qualifiers on names
Mon, 02 Apr 2012 16:06:24 +0200 huffman add lemma Suc_1
Sun, 01 Apr 2012 16:09:58 +0200 huffman removed Nat_Numeral.thy, moving all theorems elsewhere
Fri, 30 Mar 2012 16:44:23 +0200 huffman load Tools/numeral.ML in Num.thy
Fri, 30 Mar 2012 16:43:07 +0200 huffman tuned proof
Fri, 30 Mar 2012 15:56:12 +0200 huffman set up numeral reorient simproc in Num.thy
Fri, 30 Mar 2012 12:32:35 +0200 huffman replace lemmas eval_nat_numeral with a simpler reformulation
Fri, 30 Mar 2012 11:52:26 +0200 huffman new lemmas for simplifying subtraction on nat numerals
Fri, 30 Mar 2012 10:41:27 +0200 huffman move more theorems from Nat_Numeral.thy to Num.thy
Fri, 30 Mar 2012 08:15:29 +0200 huffman fix search-and-replace errors
Fri, 30 Mar 2012 09:08:29 +0200 huffman add constant pred_numeral k = numeral k - (1::nat);
Fri, 30 Mar 2012 08:10:28 +0200 huffman move lemmas from Nat_Numeral to Int.thy and Num.thy
Thu, 29 Mar 2012 14:09:10 +0200 huffman move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
Thu, 29 Mar 2012 11:47:30 +0200 huffman bootstrap Num.thy before Power.thy;
Mon, 26 Mar 2012 20:07:29 +0200 huffman fix incorrect code_modulename declarations
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
less more (0) tip