| Tue, 03 May 1994 11:30:09 +0200 |
lcp |
removal of obsolete type-declaration syntax
|
changeset |
files
|
| Sun, 24 Apr 1994 11:27:38 +0200 |
clasohm |
renamed theory files
isa94
|
changeset |
files
|
| Fri, 22 Apr 1994 21:23:14 +0200 |
clasohm |
renamed theory files
|
changeset |
files
|
| Thu, 21 Apr 1994 11:28:32 +0200 |
lcp |
tidied definitions and proofs
|
changeset |
files
|
| Thu, 21 Apr 1994 11:13:22 +0200 |
lcp |
HOL/arith.ML/plus_leD1: tidied
|
changeset |
files
|
| Tue, 19 Apr 1994 10:50:00 +0200 |
nipkow |
changed defns in hol.thy from = to ==
|
changeset |
files
|
| Wed, 06 Apr 1994 16:31:06 +0200 |
lcp |
Now simplifies before the induction
|
changeset |
files
|
| Wed, 30 Mar 1994 10:00:23 +0200 |
nipkow |
@ now associates to the right, just like #, in order to avoid loss of
|
changeset |
files
|
| Sun, 27 Mar 1994 16:43:06 +0200 |
nipkow |
Added some sums.
|
changeset |
files
|
| Sun, 27 Mar 1994 12:36:39 +0200 |
nipkow |
integrated permutative rewriting
|
changeset |
files
|
| Tue, 22 Mar 1994 19:55:29 +0100 |
nipkow |
used new field "simps" of Datatype
|
changeset |
files
|
| Tue, 22 Mar 1994 19:54:55 +0100 |
nipkow |
new field "simps" added
|
changeset |
files
|
| Tue, 22 Mar 1994 18:07:45 +0100 |
nipkow |
added dependency on datatype.ML
|
changeset |
files
|
| Tue, 22 Mar 1994 08:32:22 +0100 |
nipkow |
Updated simpsets and a few proofs.
|
changeset |
files
|
| Tue, 22 Mar 1994 08:31:58 +0100 |
nipkow |
Updated simpsets and a few proofs.
|
changeset |
files
|
| Tue, 22 Mar 1994 08:28:31 +0100 |
nipkow |
Used Datatype functor to define propositional logic terms.
|
changeset |
files
|
| Tue, 22 Mar 1994 08:26:25 +0100 |
nipkow |
simplified some proofs using ordered rewriting.
|
changeset |
files
|
| Tue, 22 Mar 1994 08:25:30 +0100 |
nipkow |
used ordered rewriting to simplify some proofs
|
changeset |
files
|
| Fri, 18 Mar 1994 20:33:32 +0100 |
nipkow |
ML-like datatype decalaration facility. Axiomatic.
|
changeset |
files
|
| Fri, 18 Mar 1994 20:32:18 +0100 |
nipkow |
added use_thy"Datatype"
|
changeset |
files
|
| Thu, 17 Mar 1994 17:02:49 +0100 |
lcp |
new type declaration syntax instead of numbers
|
changeset |
files
|
| Thu, 17 Mar 1994 14:08:08 +0100 |
lcp |
HOL/equalities/Int_Union_image, Un_Inter_image: renamed Int_Union, Un_Inter
|
changeset |
files
|
| Thu, 17 Mar 1994 11:27:29 +0100 |
clasohm |
adapted type definition to new syntax
|
changeset |
files
|
| Wed, 02 Mar 1994 12:26:55 +0100 |
clasohm |
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
|
changeset |
files
|
| Thu, 24 Feb 1994 14:45:57 +0100 |
nipkow |
typo in comment
|
changeset |
files
|
| Wed, 23 Feb 1994 10:05:35 +0100 |
nipkow |
some more sorting algorithms
|
changeset |
files
|
| Wed, 16 Feb 1994 15:13:53 +0100 |
nipkow |
added more lemmas (also to nat_ss)
|
changeset |
files
|
| Tue, 15 Feb 1994 10:05:17 +0100 |
nipkow |
deleted duplicate rewrite rules
|
changeset |
files
|
| Tue, 15 Feb 1994 07:55:22 +0100 |
nipkow |
added etac FalseE to the simplifier's solver.
|
changeset |
files
|
| Sat, 12 Feb 1994 14:46:21 +0100 |
nipkow |
added translations for "case xs of"
|
changeset |
files
|
| Fri, 11 Feb 1994 11:09:50 +0100 |
nipkow |
added ::bool in the defn of True.
|
changeset |
files
|
| Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
changeset |
files
|
| Thu, 27 Jan 1994 17:01:10 +0100 |
nipkow |
id -> idt in type of @filter and @Alls
|
changeset |
files
|
| Wed, 26 Jan 1994 17:53:27 +0100 |
nipkow |
sum: renamed case to sum_case
|
changeset |
files
|
| Mon, 24 Jan 1994 16:03:03 +0100 |
nipkow |
changed header
|
changeset |
files
|
| Mon, 24 Jan 1994 16:00:37 +0100 |
nipkow |
Verification of quicksort
|
changeset |
files
|
| Mon, 24 Jan 1994 15:59:44 +0100 |
nipkow |
added qsort
|
changeset |
files
|
| Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
changeset |
files
|
| Fri, 14 Jan 1994 12:35:27 +0100 |
lcp |
commented imageE
|
changeset |
files
|
| Fri, 07 Jan 1994 14:23:13 +0100 |
nipkow |
added let_weak_cong
|
changeset |
files
|
| Fri, 07 Jan 1994 14:22:37 +0100 |
nipkow |
added pair_eq
|
changeset |
files
|
| Wed, 05 Jan 1994 19:39:05 +0100 |
nipkow |
modified solver of HOL_ss to take the new simplifier into account: the thm to
|
changeset |
files
|
| Wed, 05 Jan 1994 19:37:07 +0100 |
nipkow |
added new rewrite rules to arith_ss
|
changeset |
files
|
| Tue, 04 Jan 1994 18:33:20 +0100 |
nipkow |
shortened use_thy section taking advantage of dependencies
|
changeset |
files
|
| Thu, 30 Dec 1993 10:19:44 +0100 |
nipkow |
added x ~: {} and x : insert(y,A) = ...
|
changeset |
files
|
| Wed, 22 Dec 1993 12:43:37 +0100 |
nipkow |
added Pair_eq to pair_ss in prod.ML
|
changeset |
files
|
| Tue, 14 Dec 1993 18:05:22 +0100 |
nipkow |
added syntax for nested lets.
|
changeset |
files
|
| Mon, 13 Dec 1993 18:43:03 +0100 |
lcp |
added mention of Subst
|
changeset |
files
|
| Fri, 03 Dec 1993 12:41:54 +0100 |
lcp |
added new example
Isabelle93
|
changeset |
files
|
| Wed, 01 Dec 1993 13:05:25 +0100 |
lcp |
HOL/llist/LList_corec_subset1: does not need induction
|
changeset |
files
|
| Tue, 30 Nov 1993 17:44:04 +0100 |
nipkow |
added pred: nat=>nat
|
changeset |
files
|
| Mon, 29 Nov 1993 18:35:02 +0100 |
nipkow |
changed simpsets
|
changeset |
files
|
| Thu, 25 Nov 1993 10:04:02 +0100 |
nipkow |
added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
|
changeset |
files
|
| Fri, 19 Nov 1993 11:36:23 +0100 |
lcp |
Trivial spacing corrections
|
changeset |
files
|
| Tue, 16 Nov 1993 14:14:22 +0100 |
clasohm |
changed use_thy's parameter to exact theory name
|
changeset |
files
|
| Tue, 09 Nov 1993 16:31:03 +0100 |
lcp |
Target "test" now depends on examples files
|
changeset |
files
|
| Tue, 09 Nov 1993 13:30:13 +0100 |
clasohm |
renamed meson-test.ML to mesontest.ML,
|
changeset |
files
|
| Tue, 09 Nov 1993 11:08:13 +0100 |
lcp |
co-induction example courtesy Jacob Frost
|
changeset |
files
|
| Wed, 03 Nov 1993 19:02:17 +0100 |
nipkow |
added append "@"
|
changeset |
files
|
| Mon, 25 Oct 1993 14:36:27 +0100 |
wenzelm |
added white-space;
|
changeset |
files
|