| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
97d0285c |
|
07-Dec-2018 |
paulson <lp15@cam.ac.uk> |
updated to modern symbols
|
| #
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
| #
7a417bae |
|
01-Aug-2017 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
36e39dcf |
|
26-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
ee8e8234 |
|
06-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
56730d74 |
|
06-Oct-2015 |
wenzelm <none@none> |
fewer aliases for toplevel theorem statements;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
6b0b29ec |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
52bca335 |
|
23-Apr-2010 |
wenzelm <none@none> |
mark schematic statements explicitly;
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
b339ba63 |
|
29-Jul-2009 |
wenzelm <none@none> |
Meson.first_order_resolve: avoid handle _;
proper context for various Meson and Metis rules and tactics
unified meson_tac/meson_claset_tac;
|
| #
2251533a |
|
20-Mar-2009 |
wenzelm <none@none> |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
| #
c5905872 |
|
16-Aug-2007 |
wenzelm <none@none> |
proper signature for Meson;
|
| #
e97486d2 |
|
26-Jun-2007 |
paulson <none@none> |
updated for metis method
|
| #
4a2a9d8e |
|
19-Apr-2007 |
paulson <none@none> |
trying to make single-step proofs work better, especially if they contain
abstraction functions. Uniform names for Skolem and Abstraction functions
|
| #
55e9d346 |
|
09-Jan-2007 |
paulson <none@none> |
simplified the resoution proofs
|
| #
b96d2be9 |
|
04-Jan-2007 |
paulson <none@none> |
improvements to proof reconstruction. Some files loaded in a different order
|
| #
ad9aba68 |
|
22-Dec-2006 |
paulson <none@none> |
revised for new make_clauses
|
| #
6f069d03 |
|
23-Oct-2006 |
paulson <none@none> |
new single-step proofs
|
| #
d7950b7f |
|
20-Oct-2006 |
paulson <none@none> |
example of a single-step proof reconstruction
|
| #
92d27b5c |
|
14-Dec-2005 |
paulson <none@none> |
modified example for new clauses
|
| #
5d69cc86 |
|
28-Jun-2005 |
paulson <none@none> |
stylistic improvements
|
| #
885dd72b |
|
24-Jun-2005 |
paulson <none@none> |
meson method taking an argument list
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
2cef3f46 |
|
20-May-2005 |
paulson <none@none> |
converted some problems to Isar format
|
| #
53e08535 |
|
07-Dec-2004 |
paulson <none@none> |
renamed attributes to lower case
|
| #
50feed4c |
|
19-Aug-2004 |
paulson <none@none> |
proof reconstruction for external ATPs
|
| #
fd9dace3 |
|
06-Aug-2004 |
paulson <none@none> |
modified resolution proof
|
| #
6f33954d |
|
28-Jun-2004 |
paulson <none@none> |
new method for explicit classical resolution
|
| #
9bef5d95 |
|
29-Oct-2003 |
paulson <none@none> |
tidying
|
| #
685d9795 |
|
08-Oct-2003 |
paulson <none@none> |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|