| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
548cd1f9 |
|
20-Jul-2017 |
blanchet <none@none> |
strengthened tactic
|
| #
65b76842 |
|
29-Jul-2016 |
Andreas Lochbihler <none@none> |
add lemmas contributed by Peter Gammie
|
| #
2cad7650 |
|
07-Apr-2016 |
traytel <none@none> |
removed duplicate lemma
|
| #
0ec920ec |
|
07-Apr-2016 |
traytel <none@none> |
derive (co)rec uniformly from (un)fold
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
23571538 |
|
07-Nov-2014 |
traytel <none@none> |
more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
eb1ed55c |
|
25-Sep-2014 |
desharna <none@none> |
generate 'corec_transfer' for codatatypes
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
8a20662e |
|
25-Sep-2014 |
desharna <none@none> |
generate 'dtor_corec_transfer' for codatatypes
|
| #
fce1041d |
|
25-Sep-2014 |
desharna <none@none> |
generate 'ctor_rec_transfer' for datatypes
|
| #
9b903e0e |
|
18-Sep-2014 |
blanchet <none@none> |
moved old 'size' generator together with 'old_datatype'
--HG--
rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML
|
| #
a3d79d09 |
|
18-Sep-2014 |
blanchet <none@none> |
moved datatype realizer to 'old_datatype' and colleagues
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
| #
823ba92f |
|
11-Sep-2014 |
blanchet <none@none> |
compile
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
| #
719673a5 |
|
09-Sep-2014 |
blanchet <none@none> |
removed debugging junk
|
| #
47c215ba |
|
09-Sep-2014 |
blanchet <none@none> |
renamed ML file and module
--HG--
rename : src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML => src/HOL/Tools/datatype_realizer.ML
|
| #
bbc86b03 |
|
09-Sep-2014 |
blanchet <none@none> |
made datatype realizer plugin work for new-style datatypes with no nesting
|
| #
75fd5395 |
|
08-Sep-2014 |
blanchet <none@none> |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
| #
a030c224 |
|
04-Sep-2014 |
blanchet <none@none> |
tweaked setup for datatype realizer
|
| #
ec4e6125 |
|
04-Sep-2014 |
blanchet <none@none> |
tuned size function generation
|
| #
0a4b950c |
|
02-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
48da5267 |
|
02-Sep-2014 |
blanchet <none@none> |
more compatibility functions
|
| #
c8de05be |
|
01-Sep-2014 |
blanchet <none@none> |
tuning
|
| #
2326a269 |
|
01-Sep-2014 |
blanchet <none@none> |
renamed BNF theories
--HG--
rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy
rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy
rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy
rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy
|