| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
8b679e5d |
|
06-Oct-2015 |
blanchet <none@none> |
tuning
|
| #
1e38ce5e |
|
12-Sep-2014 |
blanchet <none@none> |
fixed spellings
|
| #
2307f33f |
|
12-Feb-2014 |
wenzelm <none@none> |
removed odd comments -- inferred types are shown by Prover IDE;
|
| #
941cf8eb |
|
02-Dec-2011 |
wenzelm <none@none> |
more antiquotations;
|
| #
5d5ff9e2 |
|
10-Jan-2011 |
wenzelm <none@none> |
eliminated Int.toString;
|
| #
f00a3e6e |
|
08-Jan-2011 |
wenzelm <none@none> |
modernized structure Prop_Logic;
avoid ML structure aliases;
|
| #
58ede574 |
|
07-Jan-2011 |
wenzelm <none@none> |
tuned whitespace, indentation, comments;
|
| #
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
| #
33076e76 |
|
19-Aug-2010 |
haftmann <none@none> |
tuned quotes
|
| #
bbda5041 |
|
19-Aug-2010 |
haftmann <none@none> |
use antiquotations for remaining unqualified constants in HOL
|
| #
d8be8723 |
|
27-Oct-2009 |
wenzelm <none@none> |
normalized basic type abbreviations;
|
| #
26a442f9 |
|
20-Oct-2009 |
haftmann <none@none> |
curried union as canonical list operation
|
| #
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
| #
b5f3743b |
|
20-Oct-2009 |
wenzelm <none@none> |
uniform use of Integer.min/max;
|
| #
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
| #
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
| #
571f9c2d |
|
21-May-2009 |
webertj <none@none> |
implementation of definitional CNF improved
|
| #
befb5555 |
|
13-Mar-2007 |
webertj <none@none> |
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
|
| #
8eec1fce |
|
30-Aug-2006 |
webertj <none@none> |
term_of_prop_formula added
|
| #
3eb67878 |
|
09-Oct-2005 |
webertj <none@none> |
Tactics sat and satx reimplemented, several improvements
|
| #
f9ddae68 |
|
26-Jul-2005 |
webertj <none@none> |
comment modified
|
| #
88449893 |
|
25-Jul-2005 |
webertj <none@none> |
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
|
| #
6d5a361d |
|
25-Jul-2005 |
webertj <none@none> |
defcnf modified to internally use a reference
|
| #
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
| #
51ced9a9 |
|
23-Feb-2005 |
webertj <none@none> |
exception SAME removed
|
| #
5b0f1f82 |
|
19-Nov-2004 |
webertj <none@none> |
comment modified
|
| #
ca9e94d7 |
|
17-Jun-2004 |
webertj <none@none> |
improved defcnf conversion
|
| #
1b059d68 |
|
13-Jun-2004 |
webertj <none@none> |
faster defcnf conversion
|
| #
a4860138 |
|
17-May-2004 |
webertj <none@none> |
Comments fixed
|
| #
19468e1a |
|
28-Apr-2004 |
webertj <none@none> |
comments modified
|
| #
f0b6c99a |
|
10-Mar-2004 |
webertj <none@none> |
Formulas of propositional logic
|