| #
eff88f99 |
|
03-Jan-2018 |
blanchet <none@none> |
removed old 'add_datatype' ML functions
|
| #
04a2ad4d |
|
02-Jan-2018 |
blanchet <none@none> |
updated dependencies + compile
|
| #
1ab47d11 |
|
02-Jan-2018 |
blanchet <none@none> |
removed 'old_datatype' command
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
dccdabe3 |
|
03-Mar-2016 |
wenzelm <none@none> |
clarified modules;
tuned signature;
|
| #
55ef7203 |
|
17-Oct-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
44916bcd |
|
24-Sep-2015 |
wenzelm <none@none> |
explicit indication of overloaded typedefs;
|
| #
f2fecee2 |
|
03-Sep-2015 |
wenzelm <none@none> |
more general Typedef.bindings;
tuned signature;
|
| #
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
7aae2956 |
|
25-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
tuned;
|
| #
c1869c88 |
|
24-Jul-2015 |
wenzelm <none@none> |
proper context;
|
| #
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
53f968f4 |
|
01-Jun-2015 |
wenzelm <none@none> |
clarified context;
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
093cea8d |
|
31-Mar-2015 |
wenzelm <none@none> |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
| #
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
34700165 |
|
05-Mar-2015 |
wenzelm <none@none> |
tuned -- more explicit use of context;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
9e653fc8 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper proof context for typedef;
|
| #
d6623f99 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
| #
03cbd216 |
|
07-Nov-2014 |
wenzelm <none@none> |
eliminated pointless check -- command definitions are subject to theory context;
|
| #
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
| #
02b89845 |
|
08-Sep-2014 |
blanchet <none@none> |
tuned command descriptions
|
| #
e8d97a27 |
|
08-Sep-2014 |
blanchet <none@none> |
added flag to 'typedef' to allow concealed definitions
|
| #
7d13c420 |
|
01-Sep-2014 |
blanchet <none@none> |
tuned signatures
|
| #
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
|