| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
8faaa443 |
|
23-May-2016 |
wenzelm <none@none> |
embedded content may be delimited via cartouches;
|
| #
8ecffcf0 |
|
23-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
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;
|
| #
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;
|
| #
1130b1d1 |
|
11-Nov-2014 |
wenzelm <none@none> |
more markup;
|
| #
e0b2d5c0 |
|
11-Nov-2014 |
wenzelm <none@none> |
more Isar proof methods;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
82c645a3 |
|
10-Feb-2014 |
wenzelm <none@none> |
prefer vacuous definitional type classes over axiomatic ones;
|
| #
af0411f2 |
|
24-Jul-2012 |
wenzelm <none@none> |
more session ROOT files;
|
| #
2d552664 |
|
19-Mar-2012 |
wenzelm <none@none> |
modernized axiomatizations;
tuned proofs;
|
| #
f95e18b9 |
|
20-Dec-2010 |
wenzelm <none@none> |
proper identifiers for consts and types;
|
| #
b6ea9aae |
|
27-Apr-2010 |
wenzelm <none@none> |
renamed command 'defaultsort' to 'default_sort';
|
| #
458a4961 |
|
13-Mar-2010 |
wenzelm <none@none> |
removed old CVS Ids;
tuned headers;
|
| #
76ed075c |
|
15-Feb-2010 |
wenzelm <none@none> |
eliminated unnamed infixes;
|
| #
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;
|
| #
6d039539 |
|
26-Apr-2007 |
wenzelm <none@none> |
eliminated unnamed infixes;
tuned ML setup;
|
| #
b051bc99 |
|
01-Jun-2006 |
wenzelm <none@none> |
tuned;
|
| #
87c075da |
|
01-Jun-2006 |
wenzelm <none@none> |
removed obsolete ML files;
|
| #
fd125e18 |
|
03-Sep-2005 |
wenzelm <none@none> |
uses ("LCF_lemmas.ML");
|
| #
a65225cd |
|
03-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
|
| #
c4311324 |
|
21-Oct-1994 |
lcp <none@none> |
LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.
|
| #
58610472 |
|
17-Mar-1994 |
lcp <none@none> |
new type declaration syntax instead of numbers
|
| #
f253ef6a |
|
15-Sep-1993 |
clasohm <none@none> |
Initial revision
|