#
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
|