#
f413faf7 |
|
23-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
434f71f0 |
|
16-Feb-2018 |
wenzelm <none@none> |
tuned signature (again);
|
#
aad80dd3 |
|
16-Feb-2018 |
wenzelm <none@none> |
trim context of persistent data; tuned signature;
|
#
99e3d4c3 |
|
06-Dec-2017 |
wenzelm <none@none> |
prefer control symbol antiquotations;
|
#
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations --HG-- extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
#
5d91fa98 |
|
05-Apr-2017 |
Lars Hupel <lars.hupel@mytum.de> |
store totality fact in function info
|
#
2e392e73 |
|
06-Jun-2016 |
haftmann <none@none> |
explicit tagging of code equations de-baroquifies interface --HG-- extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655
|
#
cd5814d0 |
|
30-May-2016 |
wenzelm <none@none> |
tuned;
|
#
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
|
#
6bed86f1 |
|
18-Apr-2016 |
wenzelm <none@none> |
prefer internal attribute source;
|
#
9d926c7e |
|
18-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
4cf67035 |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
308c45ff |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
c7340223 |
|
17-Apr-2016 |
wenzelm <none@none> |
prefer binding over base name;
|
#
778b686b |
|
17-Apr-2016 |
wenzelm <none@none> |
tuned;
|
#
53a62d5e |
|
12-Apr-2016 |
wenzelm <none@none> |
Type_Infer.object_logic controls improvement of type inference result;
|
#
d98bbcf7 |
|
30-Mar-2016 |
wenzelm <none@none> |
reconcile object-logic constraint vs. mixfix constraint;
|
#
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
|
#
ae364dc0 |
|
04-Sep-2015 |
wenzelm <none@none> |
trim context for persistent storage; tuned signature;
|
#
a804eb03 |
|
05-Jul-2015 |
wenzelm <none@none> |
clarified context;
|
#
087ebcc2 |
|
17-Jun-2015 |
wenzelm <none@none> |
avoid dynamic parsing of hardwired strings;
|
#
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
#
03b64291 |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
de8e2f0e |
|
19-Dec-2014 |
wenzelm <none@none> |
just one data slot per program unit; tuned signature;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
4d000744 |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup; more standard module name; --HG-- rename : src/HOL/Tools/Function/context_tree.ML => src/HOL/Tools/Function/function_context_tree.ML
|
#
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
|
#
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems; modernized module name and setup;
|
#
1b8bab3e |
|
09-May-2014 |
wenzelm <none@none> |
more position markup to help locating the query context, e.g. from "Info" dockable;
|
#
3c4f4261 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
0d093612 |
|
12-Feb-2014 |
blanchet <none@none> |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
|
#
d46ef5de |
|
20-Jan-2014 |
blanchet <none@none> |
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain --HG-- rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy
|
#
47e6e8c3 |
|
31-Dec-2013 |
wenzelm <none@none> |
proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
|
#
95a2696a |
|
12-Sep-2013 |
krauss <none@none> |
omit automatic Induct.cases_pred declaration, which breaks many existing proofs
|
#
8f0efc6b |
|
08-Sep-2013 |
krauss <none@none> |
clarified
|
#
68e03336 |
|
08-Sep-2013 |
Manuel Eberl <none@none> |
generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)
|
#
6e401e29 |
|
16-Jun-2013 |
krauss <none@none> |
export dom predicate in the info record
|
#
1cdbabc0 |
|
15-Jun-2013 |
krauss <none@none> |
export cases rule in the info record
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
7fb3e27c |
|
08-Jan-2013 |
wenzelm <none@none> |
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
|
#
4463045c |
|
21-Oct-2012 |
wenzelm <none@none> |
recovered explicit error message, which was lost in b8570ea1ce25;
|
#
15463925 |
|
28-Aug-2012 |
wenzelm <none@none> |
more precise indentation;
|
#
429ef7fe |
|
23-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
#
150d8520 |
|
16-Mar-2012 |
wenzelm <none@none> |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
#
cfe58b3e |
|
19-Nov-2011 |
wenzelm <none@none> |
added ML antiquotation @{attributes};
|
#
01244fea |
|
28-Oct-2011 |
wenzelm <none@none> |
uniform Local_Theory.declaration with explicit params;
|
#
a309722d |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned signature -- refined terminology;
|
#
344a4ab5 |
|
17-Aug-2011 |
wenzelm <none@none> |
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
|
#
cc2d5210 |
|
13-Aug-2011 |
wenzelm <none@none> |
less verbosity in batch mode -- spam reduction and notable performance improvement; clarified Proof_Display.print_consts;
|
#
a40acbfc |
|
08-Aug-2011 |
wenzelm <none@none> |
slightly more uniform messages;
|
#
d4b730e6 |
|
08-Jun-2011 |
wenzelm <none@none> |
pervasive Output operations;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
8caff1de |
|
25-Feb-2011 |
krauss <none@none> |
removed support for tail-recursion from function package (now implemented by partial_function)
|
#
08819991 |
|
29-Dec-2010 |
krauss <none@none> |
function (default) is legacy feature
|
#
3bb722df |
|
26-Dec-2010 |
krauss <none@none> |
function (tailrec) is a legacy feature
|
#
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
#
0dc105bc |
|
22-Oct-2010 |
krauss <none@none> |
some cleanup in Function_Lib
|
#
0aed59d8 |
|
28-Sep-2010 |
krauss <none@none> |
no longer declare .psimps rules as [simp]. This regularly caused confusion (e.g., they show up in simp traces when the regular simp rules are disabled). In the few places where the rules are used, explicitly mentioning them actually clarifies the proof text.
|
#
dd7c556c |
|
08-Jul-2010 |
haftmann <none@none> |
tuned titles
|
#
b7e81c3e |
|
27-May-2010 |
wenzelm <none@none> |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
#
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
|
#
9995f0a4 |
|
30-Apr-2010 |
krauss <none@none> |
return updated info record after termination proof
|
#
12f7d31b |
|
28-Apr-2010 |
krauss <none@none> |
return info record (relative to auxiliary context!)
|
#
ec1f7c64 |
|
28-Apr-2010 |
krauss <none@none> |
function: sane interface for programmatic use
|
#
a1b7d02c |
|
28-Apr-2010 |
krauss <none@none> |
ML interface uses plain command names, following conventions from typedef
|
#
0d24b0ca |
|
28-Apr-2010 |
krauss <none@none> |
function: better separate Isar integration from actual functionality
|
#
14c9715d |
|
25-Apr-2010 |
wenzelm <none@none> |
modernized naming conventions of main Isar proof elements;
|
#
e61d567b |
|
11-Mar-2010 |
bulwahn <none@none> |
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
|
#
9666ec72 |
|
28-Feb-2010 |
wenzelm <none@none> |
more antiquotations;
|
#
364ef271 |
|
23-Feb-2010 |
bulwahn <none@none> |
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
|
#
6ad86b17 |
|
18-Jan-2010 |
krauss <none@none> |
function package: declare Spec_Rules for simps from total functions, but not psimps or tail-rec equations
|
#
eb23531d |
|
02-Jan-2010 |
krauss <none@none> |
new year's resolution: reindented code in function package
|
#
da7ff8d5 |
|
02-Jan-2010 |
krauss <none@none> |
provide simp and induct rules in Function.info
|
#
8da7bfa4 |
|
02-Jan-2010 |
krauss <none@none> |
more official data record Function.info
|
#
56bf35c4 |
|
17-Nov-2009 |
wenzelm <none@none> |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
#
d28e2372 |
|
13-Nov-2009 |
wenzelm <none@none> |
modernized structure Local_Theory;
|
#
21cb7d7d |
|
13-Nov-2009 |
wenzelm <none@none> |
eliminated slightly odd kind argument of LocalTheory.note(s); added LocalTheory.notes_kind as fall-back for unusual cases;
|
#
28c1be77 |
|
13-Nov-2009 |
wenzelm <none@none> |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
#
5a566ea5 |
|
10-Nov-2009 |
wenzelm <none@none> |
removed unused Quickcheck_RecFun_Simps;
|
#
296c7062 |
|
05-Nov-2009 |
wenzelm <none@none> |
adapted LocalTheory.declaration;
|
#
71c8e360 |
|
02-Nov-2009 |
krauss <none@none> |
conceal partial rules depending on config flag (i.e. when called via "fun")
|
#
50677668 |
|
02-Nov-2009 |
krauss <none@none> |
conceal "termination" rule, used only by special tools
|
#
1f5693a0 |
|
01-Nov-2009 |
wenzelm <none@none> |
modernized structure Context_Rules;
|
#
d92faf79 |
|
01-Nov-2009 |
wenzelm <none@none> |
modernized structure Rule_Cases;
|
#
78aa08c8 |
|
25-Oct-2009 |
wenzelm <none@none> |
name space groups are identified by serial, not serial_string;
|
#
1d67587c |
|
24-Oct-2009 |
krauss <none@none> |
configuration flag "partials"
|
#
f8850b31 |
|
23-Oct-2009 |
krauss <none@none> |
function package: more standard names for structures and files
|