| Thu, 23 Jul 2015 14:25:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 18:22:38 +0100 |
wenzelm |
method_setup "lem";
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 18:05:03 +0100 |
wenzelm |
proper Simplifier method setup;
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 17:56:03 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 20:15:02 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 15:41:33 +0200 |
wenzelm |
converted ML proofs from simpdata.ML;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 00:07:05 +0100 |
wenzelm |
removed legacy ML setup;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2005 15:20:08 +0200 |
wenzelm |
converted to Isar theory format;
|
file |
diff |
annotate
|
| Wed, 28 Jul 1999 13:45:33 +0200 |
paulson |
congruence rule for |-
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 18:52:48 +0200 |
paulson |
a new theory containing just an axiom needed to derive imp_cong
|
file |
diff |
annotate
|
| Tue, 20 Apr 1999 14:38:17 +0200 |
paulson |
IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 18:17:17 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 09 Oct 1996 13:32:33 +0200 |
paulson |
New unified treatment of sequent calculi by Sara Kalvala
|
file |
diff |
annotate
|