| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
| #
2759308d |
|
25-Sep-2015 |
wenzelm <none@none> |
moved remaining display.ML to more_thm.ML;
|
| #
4aa541f4 |
|
06-Apr-2015 |
wenzelm <none@none> |
@{command_spec} is superseded by @{command_keyword};
|
| #
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;
|
| #
78821146 |
|
27-Aug-2014 |
wenzelm <none@none> |
more explicit Method.modifier with reported position;
|
| #
27c03196 |
|
04-Aug-2014 |
wenzelm <none@none> |
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
|
| #
7169cd32 |
|
08-Apr-2014 |
wenzelm <none@none> |
proper context for print_tac;
|
| #
39978f9c |
|
01-Feb-2014 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
7cffb5dd |
|
17-Aug-2010 |
haftmann <none@none> |
more antiquotations
|
| #
8eb709ab |
|
20-Oct-2009 |
haftmann <none@none> |
curried inter as canonical list operation (beware of argument order)
|
| #
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
| #
886198b6 |
|
20-Jul-2009 |
wenzelm <none@none> |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
| #
e154e805 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
|
| #
5c40dae8 |
|
17-May-2008 |
wenzelm <none@none> |
structure Display: less pervasive operations;
|
| #
b959aaa7 |
|
26-Feb-2007 |
wenzelm <none@none> |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
| #
852bb740 |
|
20-Nov-2006 |
wenzelm <none@none> |
removed legacy ML setup;
|
| #
cfcb3b9c |
|
10-Oct-2006 |
haftmann <none@none> |
gen_rem(s) abandoned in favour of remove / subtract
|
| #
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
| #
c01306d6 |
|
17-Jun-2005 |
wenzelm <none@none> |
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
|
| #
e227d768 |
|
07-May-2002 |
wenzelm <none@none> |
use eq_thm_prop instead of slightly inadequate eq_thm;
|
| #
cadfdab8 |
|
27-Nov-2001 |
wenzelm <none@none> |
theory data: removed obsolete finish method;
|
| #
37c2ce11 |
|
08-Nov-2001 |
wenzelm <none@none> |
theory data: finish method;
|
| #
23d1e184 |
|
02-Aug-1999 |
wenzelm <none@none> |
cat_lines;
|
| #
950e29ac |
|
28-Jul-1999 |
paulson <none@none> |
renamed ...thm_pack... to ...pack...
|
| #
4e7e7187 |
|
27-Jul-1999 |
paulson <none@none> |
moved the modal prover to modal.ML; installed the prover using TheoryDataFun
|
| #
337c4a8c |
|
28-Dec-1998 |
paulson <none@none> |
added new arg for print_tac
|
| #
81a07728 |
|
19-Dec-1997 |
wenzelm <none@none> |
adapted to new sort function;
|
| #
76f38240 |
|
20-Oct-1997 |
wenzelm <none@none> |
adapted to qualified names;
|
| #
52ab6436 |
|
22-Jul-1997 |
paulson <none@none> |
Removal of the tactical STATE
|
| #
16062ce3 |
|
09-Oct-1996 |
paulson <none@none> |
New unified treatment of sequent calculi by Sara Kalvala
combines the old LK and Modal with the new ILL (Int. Linear Logic)
|