#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
9223db15 |
|
09-Apr-2017 |
wenzelm <none@none> |
clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;
|
#
03b18167 |
|
10-Oct-2015 |
wenzelm <none@none> |
tuned syntax -- more symbols;
|
#
56730d74 |
|
06-Oct-2015 |
wenzelm <none@none> |
fewer aliases for toplevel theorem statements;
|
#
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;
|
#
9913ba16 |
|
11-Nov-2014 |
wenzelm <none@none> |
simplifie sessions;
|
#
b4f93635 |
|
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);
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
52bca335 |
|
23-Apr-2010 |
wenzelm <none@none> |
mark schematic statements explicitly;
|
#
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids; tuned headers;
|
#
81736f36 |
|
05-Jun-2006 |
wenzelm <none@none> |
allow non-trivial schematic goals (via embedded term vars);
|
#
f03cdfbf |
|
02-Jun-2006 |
wenzelm <none@none> |
removed obsolete ML files;
|