| Wed, 17 Feb 2016 21:51:55 +0100 |
haftmann |
consolidated name
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 23:46:21 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 20 Jun 2015 16:31:44 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 11:46:03 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
ported Decision_Procs to new datatypes
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
file |
diff |
annotate
|
| Thu, 07 Aug 2014 12:17:41 +0200 |
blanchet |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Sat, 08 Mar 2014 22:21:44 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 17:07:30 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 22:10:38 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 20:07:43 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 17:36:40 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 13:54:47 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 21:52:44 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 22:42:56 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 10:33:43 +0100 |
haftmann |
regenerated
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 16:32:37 +0100 |
blanchet |
merged 'List.set' with BNF-generated 'set'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 17:01:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Sun, 02 Dec 2012 17:22:19 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Wed, 28 Nov 2012 15:59:18 +0100 |
wenzelm |
eliminated slightly odd identifiers;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:49:56 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 23:47:04 +0200 |
haftmann |
updated comment
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2011 10:36:50 +0200 |
krauss |
moved recdef package to HOL/Library/Old_Recdef.thy
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 24 Feb 2011 17:54:36 +0100 |
krauss |
recdef -> fun(ction);
|
file |
diff |
annotate
|
| Thu, 24 Feb 2011 17:38:05 +0100 |
krauss |
eliminated clones of List.upto
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 23:47:19 +0100 |
wenzelm |
tuned proofs -- eliminated prems;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:21:46 +0200 |
haftmann |
modernized primrec
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 16:09:44 +0200 |
haftmann |
diff_minus subsumes diff_def
|
file |
diff |
annotate
|
| Mon, 10 May 2010 13:58:18 +0200 |
haftmann |
less complex organization of cooper source code
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 18:34:51 +0200 |
haftmann |
do not generate code per default -- touches file of parent session
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 21:41:05 +0200 |
haftmann |
use code_reflect
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|