| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
7f6d59a0 |
|
19-Dec-2014 |
desharna <none@none> |
generate 'disc_eq_case' for Ctr_Sugars
|
| #
9b9d25bf |
|
19-Dec-2014 |
desharna <none@none> |
generate 'case_distrib' for Ctr_Sugars
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
8f51507f |
|
14-Oct-2014 |
desharna <none@none> |
add 'kind' to 'cr_sugar'
|
| #
c45d05e7 |
|
13-Oct-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
ce27dd00 |
|
13-Oct-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
6688b231 |
|
13-Oct-2014 |
wenzelm <none@none> |
module Interpretation is superseded by Plugin;
|
| #
3b70a467 |
|
09-Sep-2014 |
blanchet <none@none> |
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
|
| #
ca70b6bf |
|
09-Sep-2014 |
blanchet <none@none> |
tuned messages
|
| #
c11a8aa4 |
|
04-Sep-2014 |
blanchet <none@none> |
introduced mechanism to filter interpretations
|
| #
d36b3fcf |
|
04-Sep-2014 |
blanchet <none@none> |
fixed infinite loops in 'register' functions + more uniform API
|
| #
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|