| 2012-10-12 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| 2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 2012-04-15 |
haftmann |
centralized enriched_type declaration, thanks to in-situ available Isar commands
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| 2011-11-30 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| 2011-03-30 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| 2011-01-11 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| 2010-12-21 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| 2010-12-06 |
haftmann |
moved bootstrap of type_lifting to Fun
|
file |
diff |
annotate
|
| 2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| 2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| 2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| 2009-11-30 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| 2009-11-27 |
haftmann |
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
| 2009-11-25 |
haftmann |
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
|
file |
diff |
annotate
|
| 2009-11-12 |
haftmann |
explicit code lemmas produce nices code
|
file |
diff |
annotate
|
| 2009-03-04 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| 2009-01-21 |
haftmann |
changed import hierarchy
|
file |
diff |
annotate
|
| 2009-01-21 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
| 2008-12-27 |
krauss |
removed duplicate sum_case used only by function package;
|
file |
diff |
annotate
|
| 2008-12-09 |
huffman |
move lemmas from Numeral_Type.thy to other theories
|
file |
diff |
annotate
|
| 2008-10-24 |
haftmann |
more clever module names for code generation
|
file |
diff |
annotate
|
| 2008-10-10 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| 2008-10-07 |
haftmann |
arbitrary is undefined
|
file |
diff |
annotate
|
| 2008-09-25 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| 2008-08-24 |
haftmann |
tuned import order
|
file |
diff |
annotate
|
| 2008-08-11 |
haftmann |
moved class wellorder to theory Orderings
|
file |
diff |
annotate
|
| 2008-06-10 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| 2008-04-25 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| 2008-03-20 |
haftmann |
Product_Type.apfst and Product_Type.apsnd
|
file |
diff |
annotate
|
| 2008-03-19 |
wenzelm |
eliminated change_claset/simpset;
|
file |
diff |
annotate
|
| 2008-02-26 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| 2008-02-15 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
| 2008-01-05 |
haftmann |
more instantiation
|
file |
diff |
annotate
|
| 2007-12-17 |
berghofe |
Removed obsolete lemma size_sum.
|
file |
diff |
annotate
|
| 2007-12-05 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| 2007-11-30 |
haftmann |
more canonical attribute application
|
file |
diff |
annotate
|
| 2007-10-04 |
haftmann |
tuned datatype_codegen setup
|
file |
diff |
annotate
|
| 2007-09-26 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| 2007-09-25 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| 2007-08-15 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| 2007-08-09 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
| 2007-08-07 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
| 2007-05-09 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
file |
diff |
annotate
|
| 2007-04-24 |
berghofe |
Added intro / elim rules for prod_case.
|
file |
diff |
annotate
|
| 2007-04-20 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
| 2007-04-11 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| 2007-03-09 |
haftmann |
*** empty log message ***
|
file |
diff |
annotate
|
| 2007-02-02 |
nipkow |
a few additions and deletions
|
file |
diff |
annotate
|
| 2006-12-27 |
haftmann |
removed code generation stuff belonging to other theories
|
file |
diff |
annotate
|
| 2006-12-06 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| 2006-11-22 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
| 2006-11-17 |
haftmann |
reduced verbosity
|
file |
diff |
annotate
|
| 2006-11-17 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| 2006-11-08 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| 2006-10-31 |
haftmann |
adapted seralizer syntax
|
file |
diff |
annotate
|
| 2006-10-31 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| 2006-10-20 |
haftmann |
added reserved words for Haskell
|
file |
diff |
annotate
|