| 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
|
| Fri, 11 Nov 1994 10:35:03 +0100 |
lcp |
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
|
changeset |
files
|
| Thu, 10 Nov 1994 09:46:19 +0100 |
nipkow |
Initial revision
|
changeset |
files
|
| Wed, 09 Nov 1994 19:51:09 +0100 |
nipkow |
Added headers and made various small mods.
|
changeset |
files
|
| Wed, 09 Nov 1994 19:50:36 +0100 |
nipkow |
Added header.
|
changeset |
files
|
| Tue, 08 Nov 1994 11:21:33 +0100 |
lcp |
HOL/ROOT/HOL_dup_cs: removed as obsolete
|
changeset |
files
|
| Sun, 06 Nov 1994 21:04:50 +0100 |
clasohm |
changed loadpath
|
changeset |
files
|
| Sun, 06 Nov 1994 21:04:39 +0100 |
clasohm |
changed command for making 'test'
|
changeset |
files
|
| Fri, 04 Nov 1994 14:19:30 +0100 |
wenzelm |
rearranged theory section stuff;
|
changeset |
files
|
| Fri, 04 Nov 1994 14:17:20 +0100 |
wenzelm |
moved section parser to thy_syntax.ML;
|
changeset |
files
|
| Fri, 04 Nov 1994 14:16:39 +0100 |
wenzelm |
lnternal interface for HOL subtype definitions;
|
changeset |
files
|
| Fri, 04 Nov 1994 14:15:29 +0100 |
wenzelm |
additional theory file sections for HOL;
|
changeset |
files
|
| Fri, 04 Nov 1994 14:14:22 +0100 |
wenzelm |
abstract syntax operations for HOL;
|
changeset |
files
|
| Thu, 03 Nov 1994 11:36:54 +0100 |
nipkow |
Replaced fast_tac by simp_tac in a number of places.
|
changeset |
files
|
| Wed, 02 Nov 1994 15:26:13 +0100 |
clasohm |
added IOA files
|
changeset |
files
|
| Wed, 02 Nov 1994 11:50:09 +0100 |
clasohm |
added IOA to isabelle/HOL
|
changeset |
files
|
| Tue, 01 Nov 1994 11:00:45 +0100 |
lcp |
HOL/HOL/swap: deleted
|
changeset |
files
|
| Mon, 31 Oct 1994 17:17:48 +0100 |
lcp |
HOL/ex/cla: proofs now use deepen_tac instead of best_tac HOL_dup_cs
|
changeset |
files
|
| Thu, 13 Oct 1994 09:39:15 +0100 |
lcp |
HOL/HOL.ML/selectI2: new rule for descriptions
|
changeset |
files
|
| Wed, 12 Oct 1994 12:06:56 +0100 |
lcp |
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
|
changeset |
files
|
| Wed, 12 Oct 1994 12:00:45 +0100 |
lcp |
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
|
changeset |
files
|
| Thu, 06 Oct 1994 09:36:40 +0100 |
nipkow |
replaced some "rules" by "defs"
|
changeset |
files
|
| Tue, 04 Oct 1994 13:00:20 +0100 |
clasohm |
changed precedences to eliminate some ambiguities
Isabelle94-1
|
changeset |
files
|
| Wed, 28 Sep 1994 12:39:32 +0100 |
nipkow |
moved LList* to ex
|
changeset |
files
|
| Tue, 27 Sep 1994 13:23:04 +0100 |
nipkow |
Small simplification in add_datatype.
|
changeset |
files
|
| Mon, 26 Sep 1994 18:04:43 +0100 |
nipkow |
replaced local instantaite_types by inferT_axm
|
changeset |
files
|
| Wed, 21 Sep 1994 15:40:41 +0200 |
wenzelm |
minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections;
|
changeset |
files
|
| Fri, 16 Sep 1994 15:48:20 +0200 |
nipkow |
Definition of C was not truly prim rec because C was called inside Gamma
|
changeset |
files
|
| Thu, 15 Sep 1994 18:42:12 +0200 |
nipkow |
improved error reporting for primrec
|
changeset |
files
|
| Wed, 14 Sep 1994 16:05:28 +0200 |
wenzelm |
replaced lookup_const by Sign.const_type;
Isabelle94
|
changeset |
files
|
| Sun, 11 Sep 1994 10:31:17 +0200 |
nipkow |
Allowed string as function name in primrec header
|
changeset |
files
|
| Thu, 08 Sep 1994 11:01:45 +0200 |
lcp |
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
|
changeset |
files
|
| Wed, 07 Sep 1994 13:17:34 +0200 |
lcp |
HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
|
changeset |
files
|
| Tue, 06 Sep 1994 16:46:27 +0200 |
nipkow |
changed names
|
changeset |
files
|
| Tue, 06 Sep 1994 16:15:59 +0200 |
nipkow |
Converted rules to primrecs
|
changeset |
files
|