| #
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;
|
| #
0bf475e8 |
|
29-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
56730d74 |
|
06-Oct-2015 |
wenzelm <none@none> |
fewer aliases for toplevel theorem statements;
|
| #
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;
|
| #
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
| #
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;
|
| #
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
| #
4de86cb2 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for match_tac etc.;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
db5aeb3c |
|
16-Aug-2014 |
wenzelm <none@none> |
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
|
| #
dfab2209 |
|
05-Jul-2014 |
wenzelm <none@none> |
modernized definitions;
|
| #
2c8d6176 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
| #
0e2280bb |
|
27-Apr-2013 |
wenzelm <none@none> |
uniform Proof.context for hyp_subst_tac;
|
| #
99bd04ba |
|
23-May-2012 |
wenzelm <none@none> |
eliminated obsolete fastsimp;
|
| #
7601cf1a |
|
12-Apr-2012 |
wenzelm <none@none> |
more standard method setup;
|
| #
50fe8111 |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned Named_Thms: proper binding;
|
| #
d1a2ff7b |
|
16-Apr-2011 |
wenzelm <none@none> |
eliminated old List.nth;
tuned;
|
| #
80a964bc |
|
12-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
|
| #
7cffb5dd |
|
17-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
| #
52bca335 |
|
23-Apr-2010 |
wenzelm <none@none> |
mark schematic statements explicitly;
|
| #
d0106d17 |
|
29-Oct-2009 |
wenzelm <none@none> |
standardized filter/filter_out;
|
| #
894915ec |
|
29-Jul-2009 |
wenzelm <none@none> |
qualified Subgoal.FOCUS;
|
| #
989f3ada |
|
30-Jul-2009 |
wenzelm <none@none> |
FOCUS_PREMS as full replacement for METAHYPS, where the conclusion may still contain schematic variables;
|
| #
0b59e498 |
|
26-Jul-2009 |
wenzelm <none@none> |
tuned eval_tac: eliminated unused METAHYPS (FOCUS fails due to schematic goals);
|
| #
7b41de27 |
|
02-Jul-2009 |
wenzelm <none@none> |
renamed NamedThmsFun to Named_Thms;
simplified/unified names of instances of Named_Thms;
|
| #
be04b5a8 |
|
13-Mar-2009 |
wenzelm <none@none> |
simplified method setup;
|
| #
77d6b267 |
|
13-Mar-2009 |
wenzelm <none@none> |
unified type Proof.method and pervasive METHOD combinators;
|
| #
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
|
| #
55b075c8 |
|
30-Dec-2008 |
wenzelm <none@none> |
use regular Term.add_vars, Term.add_frees etc.;
|
| #
fe16ec1f |
|
16-Jun-2008 |
wenzelm <none@none> |
pervasive RuleInsts;
|
| #
ac45a27b |
|
14-Jun-2008 |
wenzelm <none@none> |
proper context for tactics derived from res_inst_tac;
|
| #
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;
|
| #
e24406e5 |
|
25-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
e0a03d72 |
|
03-Oct-2007 |
wenzelm <none@none> |
avoid unnamed infixes;
tuned;
|
| #
8d9b4fab |
|
29-Jul-2007 |
wenzelm <none@none> |
simplified "eval" setup via NamedThmsFun;
|
| #
b57d2603 |
|
21-Jun-2007 |
wenzelm <none@none> |
tuned proofs -- avoid implicit prems;
|
| #
b62fe892 |
|
06-May-2007 |
wenzelm <none@none> |
simplified DataFun interfaces;
|
| #
66cc6fd2 |
|
25-Jul-2006 |
wenzelm <none@none> |
Drule.merge_rules;
|
| #
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
|
| #
b8a967f4 |
|
21-Mar-1994 |
clasohm <none@none> |
changed "." to "$" to eliminate ambiguity
|
| #
f434fd7f |
|
13-Jan-1994 |
lcp <none@none> |
corrected comments
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|