#
fad9031b |
|
19-Feb-2018 |
wenzelm <none@none> |
tuned signature;
|
#
db2e05de |
|
18-Feb-2018 |
wenzelm <none@none> |
more explicit instantiate_morphism (without checks for typ / term component);
|
#
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;
|
#
5d91fa98 |
|
05-Apr-2017 |
Lars Hupel <lars.hupel@mytum.de> |
store totality fact in function info
|
#
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;
|
#
720969b0 |
|
18-Apr-2016 |
wenzelm <none@none> |
tuned;
|
#
308c45ff |
|
17-Apr-2016 |
wenzelm <none@none> |
clarified bindings;
|
#
c7340223 |
|
17-Apr-2016 |
wenzelm <none@none> |
prefer binding over base name;
|
#
f3be6ddb |
|
17-Apr-2016 |
wenzelm <none@none> |
removed pointless check (see Type_Infer.object_logic);
|
#
ae364dc0 |
|
04-Sep-2015 |
wenzelm <none@none> |
trim context for persistent storage; tuned signature;
|
#
a7d3b0ad |
|
07-Jul-2015 |
blanchet <none@none> |
have the installed termination prover take a 'quiet' flag
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
45f9fa0b |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified 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;
|
#
de8e2f0e |
|
19-Dec-2014 |
wenzelm <none@none> |
just one data slot per program unit; tuned signature;
|
#
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
#
d65030e5 |
|
19-Aug-2014 |
wenzelm <none@none> |
tuned signature -- moved type src to Token, without aliases;
|
#
9067b570 |
|
16-Aug-2014 |
wenzelm <none@none> |
updated to named_theorems; modernized module name and setup;
|
#
3c4f4261 |
|
22-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
116fd647 |
|
13-Dec-2013 |
wenzelm <none@none> |
maintain morphism names for diagnostic purposes;
|
#
ade011bf |
|
10-Nov-2013 |
haftmann <none@none> |
qualifed popular user space names
|
#
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
|
#
9ff0c5fb |
|
27-Oct-2012 |
Christian Urban <urbanc@in.tum.de> |
added function store_termination_rule to the signature, as it is used in Nominal2
|
#
63ef3daf |
|
21-Oct-2012 |
wenzelm <none@none> |
removed dead code;
|
#
2d7b73b9 |
|
21-Oct-2012 |
wenzelm <none@none> |
proper signatures;
|
#
de9fb383 |
|
15-Mar-2012 |
wenzelm <none@none> |
prefer formally checked @{keyword} parser;
|
#
2db8d06d |
|
15-Feb-2012 |
wenzelm <none@none> |
discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
|
#
61c3b64e |
|
29-Dec-2011 |
wenzelm <none@none> |
comments;
|
#
50fe8111 |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned Named_Thms: proper binding;
|
#
a309722d |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned signature -- refined terminology;
|
#
00014899 |
|
21-Aug-2011 |
wenzelm <none@none> |
tuned Parse.group: delayed failure message;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
5c43f40c |
|
24-Mar-2011 |
wenzelm <none@none> |
indentation;
|
#
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
|
#
14d00fc2 |
|
12-Dec-2010 |
krauss <none@none> |
tuned headers
|
#
a1f58d52 |
|
10-Sep-2010 |
krauss <none@none> |
improved error message for common mistake (fun f where "g x = ...")
|
#
d19dab54 |
|
05-Sep-2010 |
wenzelm <none@none> |
turned show_sorts/show_types into proper configuration options;
|
#
f4dea649 |
|
26-Aug-2010 |
wenzelm <none@none> |
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
|
#
3e123ba2 |
|
26-Aug-2010 |
wenzelm <none@none> |
theory data merge: prefer left side uniformly;
|
#
7a6b0131 |
|
17-May-2010 |
wenzelm <none@none> |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
|
#
f3ff5f68 |
|
15-May-2010 |
wenzelm <none@none> |
prefer structure Parse_Spec;
|
#
4549e8d1 |
|
05-May-2010 |
haftmann <none@none> |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
#
266cf630 |
|
28-Apr-2010 |
krauss <none@none> |
default termination prover as plain tactic
|
#
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
|
#
141c00ff |
|
19-Nov-2009 |
krauss <none@none> |
check if equations are present for all functions to avoid low-level exception later
|
#
dfa769e1 |
|
08-Nov-2009 |
wenzelm <none@none> |
adapted Generic_Data, Proof_Data; tuned;
|
#
71c8e360 |
|
02-Nov-2009 |
krauss <none@none> |
conceal partial rules depending on config flag (i.e. when called via "fun")
|
#
aa223bae |
|
01-Nov-2009 |
wenzelm <none@none> |
adapted Item_Net; tuned;
|
#
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
|