#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
5900a2cf |
|
11-Jan-2016 |
wenzelm <none@none> |
eliminated old defs;
|
#
65f3e853 |
|
01-Jan-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
7f7de75b |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
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;
|
#
50405a47 |
|
11-Nov-2014 |
wenzelm <none@none> |
more Isar proof methods;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
b8e4cb1b |
|
18-Mar-2014 |
wenzelm <none@none> |
tuned signature -- rearranged modules;
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
10eb7fb0 |
|
15-May-2011 |
wenzelm <none@none> |
simplified/unified method_setup/attribute_setup;
|
#
2f53d74a |
|
13-May-2011 |
wenzelm <none@none> |
proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
|
#
07b940f6 |
|
26-Apr-2011 |
wenzelm <none@none> |
proper antiquotations;
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
8a57ae83 |
|
29-Mar-2011 |
wenzelm <none@none> |
modernized specifications -- less axioms;
|
#
80a964bc |
|
12-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
|
#
27ff3609 |
|
06-Sep-2010 |
wenzelm <none@none> |
more antiquotations;
|
#
2b1723df |
|
28-Feb-2010 |
wenzelm <none@none> |
more antiquotations; eliminated legacy ML bindings;
|
#
aebe6a56 |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax};
|
#
3403212c |
|
08-Feb-2010 |
wenzelm <none@none> |
modernized some syntax translations;
|
#
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;
|
#
2251533a |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
#
458b7422 |
|
17-Sep-2008 |
wenzelm <none@none> |
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
|
#
bd98015c |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
#
e0a03d72 |
|
03-Oct-2007 |
wenzelm <none@none> |
avoid unnamed infixes; tuned;
|
#
95ee7518 |
|
21-Jul-2007 |
wenzelm <none@none> |
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
|
#
7501e1cc |
|
17-Jul-2006 |
wenzelm <none@none> |
removed obsolete ML files;
|
#
c046356e |
|
07-Oct-2005 |
wenzelm <none@none> |
replaced _K by dummy abstraction;
|
#
476a2058 |
|
17-Sep-2005 |
wenzelm <none@none> |
converted to Isar theory format;
|
#
1d403847 |
|
21-May-2004 |
wenzelm <none@none> |
proper use of 'syntax';
|
#
f21b472e |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
#
8ab3cd95 |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs
|
#
ca121188 |
|
06-Apr-1995 |
lcp <none@none> |
Gave tighter priorities to SUM and PROD to reduce ambiguities.
|
#
d7ecf62f |
|
04-Oct-1993 |
wenzelm <none@none> |
added parse rules for -> and *; removed ndependent_tr;
|
#
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|