| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 15:45:32 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
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, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 11:12:35 +0100 |
Andreas Lochbihler |
instantiate linorder for String.literal by lexicographic order
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Sun, 26 Aug 2012 10:20:26 +0200 |
nipkow |
fixed theory dependency
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:17 +0100 |
haftmann |
removed some legacy instantiations
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:39 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:15 +0200 |
haftmann |
moved stuff to Char_nat.thy
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:40 +0100 |
haftmann |
added instance for lattice
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:10:00 +0100 |
haftmann |
added OCaml code generation (without dictionaries)
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:27 +0100 |
haftmann |
added code generation syntax for some char combinators
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:37 +0200 |
wenzelm |
tuned presentation;
|
file |
diff |
annotate
|
| Fri, 15 Apr 2005 14:14:24 +0200 |
nipkow |
New
|
file |
diff |
annotate
|