| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
8faaa443 |
|
23-May-2016 |
wenzelm <none@none> |
embedded content may be delimited via cartouches;
|
| #
5900a2cf |
|
11-Jan-2016 |
wenzelm <none@none> |
eliminated old defs;
|
| #
65f3e853 |
|
01-Jan-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
0bf475e8 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
| #
8083303a |
|
23-Mar-2015 |
wenzelm <none@none> |
support 'for' fixes in rule_tac etc.;
|
| #
2d6c364b |
|
20-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
| #
4e1305ff |
|
19-Mar-2015 |
wenzelm <none@none> |
more position information;
|
| #
a9c547a6 |
|
10-Feb-2015 |
wenzelm <none@none> |
misc tuning;
|
| #
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
| #
bf6c9bb9 |
|
11-Nov-2014 |
wenzelm <none@none> |
more symbols;
|
| #
8478ebf4 |
|
11-Nov-2014 |
wenzelm <none@none> |
tuned whitespace;
|
| #
1130b1d1 |
|
11-Nov-2014 |
wenzelm <none@none> |
more markup;
|
| #
50405a47 |
|
11-Nov-2014 |
wenzelm <none@none> |
more Isar proof methods;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
dfab2209 |
|
05-Jul-2014 |
wenzelm <none@none> |
modernized definitions;
|
| #
b8e4cb1b |
|
18-Mar-2014 |
wenzelm <none@none> |
tuned signature -- rearranged modules;
|
| #
82c645a3 |
|
10-Feb-2014 |
wenzelm <none@none> |
prefer vacuous definitional type classes over axiomatic ones;
|
| #
63a76875 |
|
14-Dec-2013 |
wenzelm <none@none> |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
|
| #
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
| #
f705e818 |
|
09-Apr-2013 |
wenzelm <none@none> |
prefer local context;
|
| #
ecce6c57 |
|
28-Feb-2013 |
wenzelm <none@none> |
eliminated legacy 'axioms';
|
| #
99bd04ba |
|
23-May-2012 |
wenzelm <none@none> |
eliminated obsolete fastsimp;
|
| #
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
| #
07b940f6 |
|
26-Apr-2011 |
wenzelm <none@none> |
proper antiquotations;
|
| #
8a57ae83 |
|
29-Mar-2011 |
wenzelm <none@none> |
modernized specifications -- less axioms;
|
| #
3c9f234d |
|
01-Dec-2010 |
wenzelm <none@none> |
more direct use of binder_types/body_type;
|
| #
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
| #
b6ea9aae |
|
27-Apr-2010 |
wenzelm <none@none> |
renamed command 'defaultsort' to 'default_sort';
|
| #
2b1723df |
|
28-Feb-2010 |
wenzelm <none@none> |
more antiquotations;
eliminated legacy ML bindings;
|
| #
e1e22654 |
|
24-Jul-2009 |
wenzelm <none@none> |
eliminated OldGoals.prove_goal;
|
| #
b431fbef |
|
24-Jul-2009 |
wenzelm <none@none> |
explicit OldGoals;
|
| #
54f09540 |
|
23-Jul-2009 |
wenzelm <none@none> |
eliminated adhoc ML code;
|
| #
08142f67 |
|
23-Jul-2009 |
wenzelm <none@none> |
misc modernization: proper method setup instead of adhoc ML proofs;
|
| #
a4b600c4 |
|
23-Jul-2009 |
wenzelm <none@none> |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
| #
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
| #
fe16ec1f |
|
16-Jun-2008 |
wenzelm <none@none> |
pervasive RuleInsts;
|
| #
ea407404 |
|
14-Jun-2008 |
wenzelm <none@none> |
proper context for tactics derived from res_inst_tac;
|
| #
a9475b27 |
|
11-Jun-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
bd98015c |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
e0a03d72 |
|
03-Oct-2007 |
wenzelm <none@none> |
avoid unnamed infixes;
tuned;
|
| #
7501e1cc |
|
17-Jul-2006 |
wenzelm <none@none> |
removed obsolete ML files;
|
| #
476a2058 |
|
17-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
| #
f21b472e |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
| #
8ab3cd95 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
| #
268b511e |
|
21-Jun-1995 |
clasohm <none@none> |
removed \...\ inside strings
|
| #
58610472 |
|
17-Mar-1994 |
lcp <none@none> |
new type declaration syntax instead of numbers
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|