| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
97ac1d28 |
|
01-Jan-2016 |
wenzelm <none@none> |
more symbols;
|
| #
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
426ed185 |
|
13-Sep-2014 |
blanchet <none@none> |
ported Imperative HOL to new datatypes
|
| #
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
| #
9fc7f521 |
|
09-Sep-2014 |
blanchet <none@none> |
half-ported Imperative HOL to new datatypes
|
| #
d2ddb3a1 |
|
09-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
|
| #
84985a9a |
|
06-Aug-2014 |
blanchet <none@none> |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
| #
713cd402 |
|
13-Mar-2014 |
nipkow <none@none> |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893
|
| #
ce43d47f |
|
19-Feb-2014 |
blanchet <none@none> |
merged 'List.set' with BNF-generated 'set'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
49681fa0 |
|
20-Aug-2013 |
krauss <none@none> |
replaced use of obsolete MREC by partial_function (heap)
|
| #
3e0fffd8 |
|
24-Feb-2013 |
wenzelm <none@none> |
prefer stateless 'ML_val' for tests;
|
| #
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
--HG--
extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
| #
8f5e99df |
|
28-Dec-2012 |
haftmann <none@none> |
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
|
| #
60ef6e49 |
|
23-Jul-2012 |
haftmann <none@none> |
more correct import
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
31b925ba |
|
14-Jan-2011 |
wenzelm <none@none> |
more precise import;
eliminated global prems;
|
| #
7ab99529 |
|
22-Nov-2010 |
haftmann <none@none> |
renamed slightly ambivalent crel to effect
|
| #
b1757d21 |
|
25-Oct-2010 |
krauss <none@none> |
use partial_function instead of MREC combinator; curried rev'
|
| #
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
| #
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
| #
ca333cbd |
|
13-Aug-2010 |
haftmann <none@none> |
robustified proof
|
| #
9d6da406 |
|
28-Jul-2010 |
haftmann <none@none> |
intermediate operation avoids invariance problem in Scala
|
| #
9aac70f7 |
|
29-Jul-2010 |
haftmann <none@none> |
checking Scala_imp
|
| #
1820aca2 |
|
26-Jul-2010 |
haftmann <none@none> |
reactivated Scala check
|
| #
d3f4e2a1 |
|
24-Jul-2010 |
haftmann <none@none> |
temporarily deactivating check for Scala
|
| #
95d659be |
|
19-Jul-2010 |
haftmann <none@none> |
check code generation for Scala
|
| #
0e4cddee |
|
14-Jul-2010 |
haftmann <none@none> |
avoid ambiguities; tuned
|
| #
1c59814f |
|
14-Jul-2010 |
haftmann <none@none> |
avoid export_code ... file -
|
| #
e210c470 |
|
12-Jul-2010 |
krauss <none@none> |
Heap_Monad uses Monad_Syntax
|
| #
c66b6c29 |
|
12-Jul-2010 |
haftmann <none@none> |
spelt out relational framework in a consistent way
|
| #
55a5de32 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
| #
d0f1288b |
|
08-Jul-2010 |
haftmann <none@none> |
dropped ancient in-place compilation of SML; more tests
|
| #
873b480f |
|
06-Jul-2010 |
haftmann <none@none> |
refactored reference operations
|
| #
67404e75 |
|
05-Jul-2010 |
haftmann <none@none> |
simplified representation of monad type
|
| #
e03f464e |
|
08-Apr-2010 |
bulwahn <none@none> |
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
|
| #
24805c77 |
|
01-Mar-2010 |
wenzelm <none@none> |
eliminated hard tabs;
|
| #
16f52a0a |
|
08-Feb-2010 |
haftmann <none@none> |
avoid upto in generated code (is infix operator in library.ML)
|
| #
0da9cb10 |
|
10-Dec-2009 |
bulwahn <none@none> |
added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
|