webertj [Thu, 25 Nov 2004 20:33:35 +0100] rev 15335
minor code refactoring (typ_of_dtyp, size_of_dtyp)
webertj [Thu, 25 Nov 2004 19:25:03 +0100] rev 15334
exception CANNOT_INTERPRET removed (not needed anymore since the stlc_interpreter can interpret any term)
webertj [Thu, 25 Nov 2004 19:04:32 +0100] rev 15333
comments edited
webertj [Thu, 25 Nov 2004 14:44:52 +0100] rev 15332
added ZCHAFF_VERSION
webertj [Thu, 25 Nov 2004 14:38:37 +0100] rev 15331
added ZCHAFF_VERSION
paulson [Thu, 25 Nov 2004 12:39:12 +0100] rev 15330
ML
webertj [Wed, 24 Nov 2004 19:51:33 +0100] rev 15329
Removed a "Matches are not exhaustive" warning
nipkow [Wed, 24 Nov 2004 11:13:00 +0100] rev 15328
mod because of change in finite set induction
nipkow [Wed, 24 Nov 2004 11:12:10 +0100] rev 15327
changed the order of !!-quantifiers in finite set induction.
In Isar you can now write (insert x F) rather than the counterintuitive
(insert F x).
berghofe [Wed, 24 Nov 2004 10:37:38 +0100] rev 15326
Made test_term escape special characters in strings that caused the
ML compiler to fail.
berghofe [Wed, 24 Nov 2004 10:32:33 +0100] rev 15325
Functions nat_to_bv and bv_to_nat now really operate on natural numbers.
berghofe [Wed, 24 Nov 2004 10:30:19 +0100] rev 15324
Added EfficientNat
berghofe [Wed, 24 Nov 2004 10:29:44 +0100] rev 15323
Code generator plug-in for implementing natural numbers by integers.
berghofe [Wed, 24 Nov 2004 10:28:09 +0100] rev 15322
Added Library/EfficientNat
berghofe [Wed, 24 Nov 2004 10:27:24 +0100] rev 15321
Reimplemented some operations on "code lemma" table to avoid that code
lemmas get lost during merge.
berghofe [Wed, 24 Nov 2004 10:23:36 +0100] rev 15320
New theorem zpower_int
nipkow [Wed, 24 Nov 2004 08:43:41 +0100] rev 15319
*** empty log message ***
obua [Tue, 23 Nov 2004 18:58:59 +0100] rev 15318
prettier proof of setsum_diff
webertj [Tue, 23 Nov 2004 17:47:37 +0100] rev 15317
HTML conformity
nipkow [Tue, 23 Nov 2004 16:43:03 +0100] rev 15316
renamed 1 lemmas
nipkow [Tue, 23 Nov 2004 16:42:54 +0100] rev 15315
renamed 2 lemmas
obua [Tue, 23 Nov 2004 15:50:27 +0100] rev 15314
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
webertj [Tue, 23 Nov 2004 15:36:39 +0100] rev 15313
external solvers may now overwrite existing temporary files
nipkow [Tue, 23 Nov 2004 15:32:11 +0100] rev 15312
added lemma
obua [Tue, 23 Nov 2004 15:25:39 +0100] rev 15311
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
nipkow [Tue, 23 Nov 2004 14:21:24 +0100] rev 15310
*** empty log message ***
nipkow [Tue, 23 Nov 2004 09:08:35 +0100] rev 15309
generalized lemma
nipkow [Tue, 23 Nov 2004 08:58:32 +0100] rev 15308
added lemma
paulson [Mon, 22 Nov 2004 13:52:27 +0100] rev 15307
indentation
nipkow [Mon, 22 Nov 2004 11:54:08 +0100] rev 15306
fixed proof
nipkow [Mon, 22 Nov 2004 11:53:56 +0100] rev 15305
added lemmas
nipkow [Sun, 21 Nov 2004 18:39:25 +0100] rev 15304
Added more lemmas
nipkow [Sun, 21 Nov 2004 15:44:20 +0100] rev 15303
added lemmas
nipkow [Sun, 21 Nov 2004 12:52:03 +0100] rev 15302
Restructured List and added "rotate"
webertj [Fri, 19 Nov 2004 17:52:07 +0100] rev 15301
comment modified
paulson [Fri, 19 Nov 2004 17:31:49 +0100] rev 15300
moved and renamed Integ/Equiv.thy
webertj [Fri, 19 Nov 2004 15:05:10 +0100] rev 15299
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
chaieb [Fri, 19 Nov 2004 14:00:31 +0100] rev 15298
Barith removed
VS: ----------------------------------------------------------------------
webertj [Thu, 18 Nov 2004 18:46:09 +0100] rev 15297
imports (new syntax for theory headers)
berghofe [Thu, 18 Nov 2004 14:02:29 +0100] rev 15296
Tuned.
kleing [Wed, 17 Nov 2004 22:18:52 +0100] rev 15295
replace strangely encode space characters by
kleing [Wed, 17 Nov 2004 22:17:51 +0100] rev 15294
replaced strangely encoded space characters by
webertj [Wed, 17 Nov 2004 19:25:34 +0100] rev 15293
removed explicit mentioning of zChaffs version number
webertj [Wed, 17 Nov 2004 16:24:07 +0100] rev 15292
minor changes (comments/code refactoring)
kleing [Wed, 17 Nov 2004 07:35:50 +0100] rev 15291
removed Exercises document (available on separate web site now)
kleing [Wed, 17 Nov 2004 07:35:14 +0100] rev 15290
removed exercised document
aspinall [Tue, 16 Nov 2004 20:20:14 +0100] rev 15289
Markup obtain as introducing a nested goal.
paulson [Mon, 15 Nov 2004 18:21:34 +0100] rev 15288
removed a "clone" (duplicate code)
webertj [Mon, 15 Nov 2004 17:04:11 +0100] rev 15287
minor rewording
aspinall [Mon, 15 Nov 2004 13:51:43 +0100] rev 15286
Add <undoitem> for theory-state undos.
paulson [Mon, 15 Nov 2004 12:13:14 +0100] rev 15285
Renamed some variables to eliminate conflicts with constants.
Introduced some abbreviations (following TPTP axiom sets) to reduce the
amount of repetition.
Uncommented some examples, which increases the runtime somewhat.
webertj [Sun, 14 Nov 2004 01:56:58 +0100] rev 15284
*** empty log message ***
webertj [Sun, 14 Nov 2004 01:40:27 +0100] rev 15283
DOCTYPE declaration added
webertj [Sat, 13 Nov 2004 17:30:03 +0100] rev 15282
Exercises added
nipkow [Sat, 13 Nov 2004 07:47:34 +0100] rev 15281
More lemmas
webertj [Fri, 12 Nov 2004 20:55:04 +0100] rev 15280
minor code refactoring