| Tue, 14 Mar 1995 09:42:49 +0100 |
nipkow |
added "exit 1"
|
changeset |
files
|
| Mon, 13 Mar 1995 09:41:20 +0100 |
nipkow |
Removed unecessary type constraint because instantiations do not freeze type
|
changeset |
files
|
| Wed, 08 Mar 1995 17:22:28 +0100 |
nipkow |
Added dependencies on ../Provers/hypsubst.ML and removed those on
|
changeset |
files
|
| Wed, 08 Mar 1995 13:06:44 +0100 |
nipkow |
Enforced partial evaluation of mk_case_split_tac
|
changeset |
files
|
| Wed, 01 Mar 1995 17:44:05 +0100 |
lcp |
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
|
changeset |
files
|
| Wed, 01 Mar 1995 17:37:09 +0100 |
lcp |
Proofs of inv1 and inv4 now use less_le_trans instead of
|
changeset |
files
|
| Wed, 01 Mar 1995 17:32:10 +0100 |
lcp |
Renamed plus_leD1 to add_leD1.
|
changeset |
files
|
| Wed, 01 Mar 1995 13:26:50 +0100 |
lcp |
Proved inj_onto_iff
|
changeset |
files
|
| Tue, 28 Feb 1995 10:52:55 +0100 |
lcp |
No longer calls maketest; instead, the Makefile writes the file
|
changeset |
files
|
| Tue, 28 Feb 1995 10:48:46 +0100 |
lcp |
Re-organised to perform the tests independently. Now test
|
changeset |
files
|
| Tue, 28 Feb 1995 02:02:34 +0100 |
lcp |
Installation of Integ (ported from ZF by Mattolini)
|
changeset |
files
|
| Tue, 28 Feb 1995 02:00:28 +0100 |
lcp |
Proved less_eq_Suc_add and add_left_cancel (cf left_plus_cancel on
|
changeset |
files
|
| Mon, 27 Feb 1995 17:20:33 +0100 |
lcp |
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
|
changeset |
files
|
| Mon, 27 Feb 1995 16:46:38 +0100 |
lcp |
Installation of Integ (ported from ZF by Mattolini)
|
changeset |
files
|
| Mon, 27 Feb 1995 16:36:17 +0100 |
lcp |
Installation of Integ (ported from ZF by Mattolini)
|
changeset |
files
|
| Sun, 19 Feb 1995 15:04:39 +0100 |
nipkow |
Reorganized/optimized datatype definitions.
|
changeset |
files
|
| Thu, 16 Feb 1995 08:56:44 +0100 |
nipkow |
pair_ss -> prod_ss.
|
changeset |
files
|
| Thu, 16 Feb 1995 08:56:21 +0100 |
nipkow |
Removed pair_ss because identical to prod_ss.
|
changeset |
files
|
| Mon, 13 Feb 1995 15:12:08 +0100 |
nipkow |
Added "flat"
|
changeset |
files
|
| Wed, 08 Feb 1995 14:06:37 +0100 |
nipkow |
Norbert's update allowing nested calls in primrec.
|
changeset |
files
|
| Wed, 08 Feb 1995 11:34:11 +0100 |
nipkow |
More rewrite rules.
|
changeset |
files
|
| Fri, 03 Feb 1995 16:21:45 +0100 |
nipkow |
Add dependence on ex/String.thy/ML
|
changeset |
files
|
| Fri, 03 Feb 1995 16:19:45 +0100 |
nipkow |
Added Markus Wenzel's string representation.
|
changeset |
files
|
| Wed, 01 Feb 1995 17:18:00 +0100 |
nipkow |
Simplified proof.
|
changeset |
files
|
| Wed, 01 Feb 1995 17:17:35 +0100 |
nipkow |
The thm if(P,Q,R) now yields the two conditional rewrite rules P ==> Q and
|
changeset |
files
|
| Mon, 30 Jan 1995 16:32:32 +0100 |
nipkow |
Added Un_empty (also to set_ss)
|
changeset |
files
|
| Sun, 29 Jan 1995 14:02:17 +0100 |
nipkow |
Added some simplifications for ? x.
|
changeset |
files
|
| Thu, 26 Jan 1995 10:41:21 +0100 |
nipkow |
Added "nth" and some lemmas.
|
changeset |
files
|
| Wed, 14 Dec 1994 11:17:18 +0100 |
clasohm |
added bind_thm for theorems made by "standard ..."
Isabelle94-2
|
changeset |
files
|
| Wed, 14 Dec 1994 10:32:07 +0100 |
wenzelm |
improved primrec: now calls store_thm;
|
changeset |
files
|
| Fri, 09 Dec 1994 13:39:05 +0100 |
clasohm |
removed HOL_Lemmas structure and added qed_goal
|
changeset |
files
|
| Thu, 08 Dec 1994 12:50:38 +0100 |
clasohm |
replaced store_thm by bind_thm
|
changeset |
files
|
| Wed, 07 Dec 1994 14:12:27 +0100 |
nipkow |
Added (? x. x=t & P) = P to the simpset.
|
changeset |
files
|
| Wed, 07 Dec 1994 14:11:22 +0100 |
nipkow |
Removed a local lemma which is now part of HOL_ss.
|
changeset |
files
|
| Fri, 02 Dec 1994 16:13:34 +0100 |
nipkow |
Moved the old List to ex and replaced it by one defined via
|
changeset |
files
|
| Fri, 02 Dec 1994 16:09:49 +0100 |
nipkow |
Moved HOL/List to HOL/ex/SList (strict list).
|
changeset |
files
|
| Fri, 02 Dec 1994 11:43:20 +0100 |
nipkow |
small updates because datatype list is now used. In particular Nil -> []
|
changeset |
files
|
| Fri, 02 Dec 1994 10:26:59 +0100 |
nipkow |
list_ind_tac -> list.induct_tac
|
changeset |
files
|
| Thu, 01 Dec 1994 17:35:03 +0100 |
nipkow |
Added dependency on thy_syntax.ML
|
changeset |
files
|
| Mon, 28 Nov 1994 16:45:29 +0100 |
nipkow |
Fixed small bug in print-translation for set comprehension.
|
changeset |
files
|
| Mon, 28 Nov 1994 14:42:42 +0100 |
wenzelm |
adapted to 'subtype' section;
|
changeset |
files
|
| Fri, 25 Nov 1994 20:07:22 +0100 |
nipkow |
added IMP/Properties
|
changeset |
files
|
| Fri, 25 Nov 1994 20:06:15 +0100 |
nipkow |
Proved determinism.
|
changeset |
files
|
| Fri, 25 Nov 1994 16:24:18 +0100 |
wenzelm |
minor changes according to new hologic;
|
changeset |
files
|
| Fri, 25 Nov 1994 14:39:13 +0100 |
wenzelm |
replaced ["term"] by termS;
|
changeset |
files
|
| Fri, 25 Nov 1994 14:21:14 +0100 |
wenzelm |
adapted to 'subtype' section;
|
changeset |
files
|
| Fri, 25 Nov 1994 13:35:32 +0100 |
nipkow |
added id_in_pair_conv
|
changeset |
files
|
| Fri, 25 Nov 1994 13:34:33 +0100 |
nipkow |
Removed obsolete induction package
|
changeset |
files
|
| Fri, 25 Nov 1994 13:33:27 +0100 |
nipkow |
removed Sum-rules
|
changeset |
files
|
| Fri, 25 Nov 1994 11:10:26 +0100 |
lcp |
checks that the recursive sets are Consts before taking
|
changeset |
files
|
| Fri, 25 Nov 1994 09:59:51 +0100 |
nipkow |
renamed term_induct/2 -> Term_induct/2
|
changeset |
files
|
| Fri, 25 Nov 1994 09:12:16 +0100 |
clasohm |
replaced prove_goal by qed_goal
|
changeset |
files
|
| Thu, 24 Nov 1994 20:31:09 +0100 |
nipkow |
rules -> defs
|
changeset |
files
|
| Thu, 24 Nov 1994 20:11:40 +0100 |
nipkow |
The collection of theories required for inductive definitions.
|
changeset |
files
|
| Thu, 24 Nov 1994 20:00:52 +0100 |
nipkow |
Trancl.{thy,ML} was missing
|
changeset |
files
|
| Wed, 23 Nov 1994 15:09:44 +0100 |
wenzelm |
moved parser stuff to thy_syntax.ML;
|
changeset |
files
|
| Wed, 23 Nov 1994 10:41:42 +0100 |
wenzelm |
add_subtype now adds constant definition for the representing set;
|
changeset |
files
|
| Wed, 23 Nov 1994 10:37:27 +0100 |
wenzelm |
moved remaining thy syntax stuff to thy_syntax.ML;
|
changeset |
files
|
| Wed, 23 Nov 1994 10:36:03 +0100 |
wenzelm |
added 'datatype' and 'primrec';
|
changeset |
files
|
| Mon, 21 Nov 1994 17:50:34 +0100 |
clasohm |
replaced 'val ... = result()' by 'qed "..."'
|
changeset |
files
|