| Thu, 02 Jan 2025 08:37:55 +0100 |
haftmann |
refined syntax for code_reserved
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Fri, 01 Jan 2016 14:44:52 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sat, 13 Sep 2014 18:08:45 +0200 |
blanchet |
ported Imperative HOL to new datatypes
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
half-ported Imperative HOL 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
|
| Thu, 13 Mar 2014 07:07:07 +0100 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
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:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 11:21:49 +0200 |
krauss |
replaced use of obsolete MREC by partial_function (heap)
|
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
|
| Fri, 28 Dec 2012 10:25:59 +0100 |
haftmann |
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 09:26:55 +0200 |
haftmann |
more correct import
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:43:04 +0100 |
wenzelm |
more precise import;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 09:37:39 +0100 |
haftmann |
renamed slightly ambivalent crel to effect
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:19:02 +0200 |
krauss |
use partial_function instead of MREC combinator; curried rev'
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 13 Aug 2010 16:40:47 +0200 |
haftmann |
robustified proof
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 12:28:45 +0200 |
haftmann |
intermediate operation avoids invariance problem in Scala
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 09:56:59 +0200 |
haftmann |
checking Scala_imp
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:09:45 +0200 |
haftmann |
reactivated Scala check
|
file |
diff |
annotate
|
| Sat, 24 Jul 2010 18:08:43 +0200 |
haftmann |
temporarily deactivating check for Scala
|
file |
diff |
annotate
|
| Mon, 19 Jul 2010 11:55:42 +0200 |
haftmann |
check code generation for Scala
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:45:30 +0200 |
haftmann |
avoid ambiguities; tuned
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:13:14 +0200 |
haftmann |
avoid export_code ... file -
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 12:00:11 +0200 |
krauss |
Heap_Monad uses Monad_Syntax
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:05:08 +0200 |
haftmann |
spelt out relational framework in a consistent way
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 17:23:05 +0200 |
haftmann |
dropped ancient in-place compilation of SML; more tests
|
file |
diff |
annotate
|
| Tue, 06 Jul 2010 09:21:15 +0200 |
haftmann |
refactored reference operations
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 14:34:28 +0200 |
haftmann |
simplified representation of monad type
|
file |
diff |
annotate
|
| Thu, 08 Apr 2010 08:17:27 +0200 |
bulwahn |
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 21:41:35 +0100 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 14:12:50 +0100 |
haftmann |
avoid upto in generated code (is infix operator in library.ML)
|
file |
diff |
annotate
|
| Thu, 10 Dec 2009 11:58:26 +0100 |
bulwahn |
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
|
file |
diff |
annotate
|