| Thu, 29 Jun 1995 12:29:58 +0200 |
clasohm |
changed HOL to Old_HOL
Isabelle94-4
|
changeset |
files
|
| Wed, 21 Jun 1995 15:12:40 +0200 |
clasohm |
removed \...\ inside strings
|
changeset |
files
|
| Fri, 14 Apr 1995 11:23:33 +0200 |
lcp |
Simplified some proofs and made them work for new hyp_subst_tac.
Isabelle94-3
|
changeset |
files
|
| Thu, 06 Apr 1995 11:52:05 +0200 |
lcp |
Removed the "exit 1" calls, since now the
|
changeset |
files
|
| Thu, 06 Apr 1995 11:49:42 +0200 |
lcp |
Deleted extra space in clos_mk.
|
changeset |
files
|
| Thu, 06 Apr 1995 11:47:00 +0200 |
lcp |
Simplified some proofs and made them work for new hyp_subst_tac.
|
changeset |
files
|
| Thu, 06 Apr 1995 11:37:43 +0200 |
lcp |
Ran expandshort
|
changeset |
files
|
| Thu, 06 Apr 1995 11:35:33 +0200 |
lcp |
Removed the "exit 1" calls, since now the
|
changeset |
files
|
| Thu, 06 Apr 1995 11:32:47 +0200 |
lcp |
Deleted some useless things and made proofs of
|
changeset |
files
|
| Thu, 06 Apr 1995 11:27:54 +0200 |
lcp |
Removed the "exit 1" calls, since now the
|
changeset |
files
|
| Thu, 06 Apr 1995 11:24:11 +0200 |
lcp |
Set up for new hyp_subst_tac.
|
changeset |
files
|
| Thu, 06 Apr 1995 11:21:13 +0200 |
lcp |
Changed proof of lessE for new hyp_subst_tac
|
changeset |
files
|
| Thu, 06 Apr 1995 11:18:02 +0200 |
lcp |
Added Id: line
|
changeset |
files
|
| Fri, 31 Mar 1995 15:09:21 +0200 |
wenzelm |
replaced 'arities' by 'instance';
|
changeset |
files
|
| Thu, 30 Mar 1995 13:39:36 +0200 |
lcp |
Defined addss to perform simplification in a claset.
|
changeset |
files
|
| Tue, 28 Mar 1995 12:48:46 +0200 |
clasohm |
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
|
changeset |
files
|
| Mon, 27 Mar 1995 18:30:04 +0200 |
nipkow |
Added recursion equations for foldl to list_ss.
|
changeset |
files
|
| Fri, 17 Mar 1995 15:48:55 +0100 |
nipkow |
Added a few thms to nat_ss and list_ss
|
changeset |
files
|
| Wed, 15 Mar 1995 10:44:26 +0100 |
lcp |
Now calls exit_use instead of use, for prompt failure if errors are detected.
|
changeset |
files
|
| Tue, 14 Mar 1995 09:43:12 +0100 |
nipkow |
Removed some type constraints
|
changeset |
files
|
| 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
|