| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
33069e0b |
|
02-Jan-2018 |
blanchet <none@none> |
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
|
| #
1ab47d11 |
|
02-Jan-2018 |
blanchet <none@none> |
removed 'old_datatype' command
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
acc65bc7 |
|
19-Apr-2017 |
wenzelm <none@none> |
tuned imports;
|
| #
744b34a2 |
|
11-Jan-2016 |
wenzelm <none@none> |
eliminated old defs;
|
| #
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
| #
7c503729 |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <*>;
|
| #
26ece69c |
|
05-Nov-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
f81a74f2 |
|
19-Sep-2014 |
blanchet <none@none> |
keep obsolete interpretations in Main, to avoid merge trouble
|
| #
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
|
| #
392cced7 |
|
18-Sep-2014 |
blanchet <none@none> |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
* * *
made example compile again
--HG--
rename : src/HOL/Old_Datatype.thy => src/HOL/Library/Old_Datatype.thy
|