| Sat, 19 Mar 2016 16:53:09 +0100 |
haftmann |
unified CHAR with CHR syntax
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:01 +0100 |
haftmann |
moved
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 17:52:52 +0100 |
haftmann |
more direct bootstrap of char type, still retaining the nibble representation for syntax
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:02:43 +0200 |
blanchet |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:44:51 +0100 |
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
|
| Thu, 05 Feb 2015 19:44:14 +0100 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 19:44:13 +0100 |
haftmann |
explicit type annotation avoids problems with Haskell type inference
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 15:07:53 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
use balanced tuples in 'primcorec'
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:59:25 +0100 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:56:38 +0100 |
Andreas Lochbihler |
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 15 Jan 2014 23:25:28 +0100 |
wenzelm |
added \<newline> symbol, which is used for char/string literals in HOL;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 11:10:05 +0100 |
Andreas Lochbihler |
setup lifting/transfer for String.literal
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 15:33:20 +0200 |
Andreas Lochbihler |
add congruence rule to prevent code_simp from looping
|
file |
diff |
annotate
|