| Sat, 02 Jan 2016 18:48:45 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 23:28:49 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:58:35 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Mon, 05 Aug 2013 17:52:07 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 19:23:51 +0200 |
haftmann |
abandoned almost redundant *_foldr lemmas
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 22:17:10 +0100 |
haftmann |
incorporated More_Set and More_List into the Main body -- to be consolidated later
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 17:40:43 +0100 |
haftmann |
dropped Executable_Set wrapper theory
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 05 Aug 2011 14:16:44 +0200 |
Andreas Lochbihler |
replace old SML code generator by new code generator in MicroJava/JVM and /BV
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2010 20:19:00 +0200 |
nipkow |
nat_number -> eval_nat_numeral
|
file |
diff |
annotate
|
| Thu, 20 May 2010 16:40:29 +0200 |
haftmann |
renamed List_Set to the now more appropriate More_Set
|
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
|
| Thu, 11 Feb 2010 00:45:02 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 14:37:23 +0100 |
haftmann |
backported parts of abstract byte code verifier from AFP/Jinja
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 16:17:55 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:18:57 +0200 |
haftmann |
explicit Set constructor for code generated for sets
|
file |
diff |
annotate
|
| Mon, 18 May 2009 23:15:38 +0200 |
nipkow |
fine-tuned elimination of comprehensions involving x=t.
|
file |
diff |
annotate
|
| Sat, 16 May 2009 17:44:11 +0200 |
nipkow |
proof tuned
|
file |
diff |
annotate
|
| Sat, 16 May 2009 11:28:02 +0200 |
nipkow |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:25 +0200 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:54:51 +0200 |
wenzelm |
theory header: fixed import;
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 17:46:31 +0200 |
wenzelm |
theory header: more precise imports;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|