| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 11:34:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 11:16:47 +0200 |
blanchet |
fixed spellings
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 13:31:18 +0100 |
wenzelm |
removed odd comments -- inferred types are shown by Prover IDE;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Sat, 08 Jan 2011 16:01:51 +0100 |
wenzelm |
modernized structure Prop_Logic;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 17:07:00 +0100 |
wenzelm |
tuned whitespace, indentation, comments;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 17:34:00 +0100 |
wenzelm |
normalized basic type abbreviations;
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 12:02:56 +0200 |
haftmann |
curried union as canonical list operation
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 20:54:31 +0200 |
wenzelm |
uniform use of Integer.min/max;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 21 May 2009 15:25:26 +0100 |
webertj |
implementation of definitional CNF improved
|
file |
diff |
annotate
|
| Wed, 14 Mar 2007 01:35:02 +0100 |
webertj |
is_nnf/is_cnf added, defcnf does nothing now if the formula already is in CNF
|
file |
diff |
annotate
|
| Thu, 31 Aug 2006 02:59:08 +0200 |
webertj |
term_of_prop_formula added
|
file |
diff |
annotate
|
| Sun, 09 Oct 2005 17:06:03 +0200 |
webertj |
Tactics sat and satx reimplemented, several improvements
|
file |
diff |
annotate
|
| Tue, 26 Jul 2005 14:14:13 +0200 |
webertj |
comment modified
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 21:40:43 +0200 |
webertj |
defcnf renamed to auxcnf, new defcnf algorithm added, simplify added
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 15:51:30 +0200 |
webertj |
defcnf modified to internally use a reference
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Wed, 23 Feb 2005 15:00:03 +0100 |
webertj |
exception SAME removed
|
file |
diff |
annotate
|
| Fri, 19 Nov 2004 17:52:07 +0100 |
webertj |
comment modified
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 21:58:51 +0200 |
webertj |
improved defcnf conversion
|
file |
diff |
annotate
|
| Sun, 13 Jun 2004 17:57:35 +0200 |
webertj |
faster defcnf conversion
|
file |
diff |
annotate
|
| Mon, 17 May 2004 14:05:06 +0200 |
webertj |
Comments fixed
|
file |
diff |
annotate
|
| Wed, 28 Apr 2004 10:45:35 +0200 |
webertj |
comments modified
|
file |
diff |
annotate
|
| Wed, 10 Mar 2004 20:27:56 +0100 |
webertj |
Formulas of propositional logic
|
file |
diff |
annotate
|