| 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
|
| Tue, 06 Sep 1994 13:24:29 +0200 |
lcp |
corrected comment re treatment of types such as (bool*bool)*bool
|
changeset |
files
|
| Tue, 06 Sep 1994 10:56:54 +0200 |
lcp |
HOL/ex/PropLog.thy: tidied
|
changeset |
files
|
| Tue, 06 Sep 1994 10:54:46 +0200 |
lcp |
HOL/ind_syntax/factors: now returns only factors in the product type that
|
changeset |
files
|
| Wed, 31 Aug 1994 17:50:59 +0200 |
nipkow |
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
|
changeset |
files
|
| Wed, 31 Aug 1994 16:25:19 +0200 |
nipkow |
Renamed a few types and vars
|
changeset |
files
|
| Wed, 31 Aug 1994 15:15:54 +0200 |
nipkow |
Equivalence of op. and den. sem. for simple while language.
|
changeset |
files
|
| Tue, 30 Aug 1994 10:05:46 +0200 |
nipkow |
Updated PL to PropLog using Larrys ind. defs.
|
changeset |
files
|
| Tue, 30 Aug 1994 10:04:49 +0200 |
nipkow |
New version of datatype.ML with primrec (Norbert).
|
changeset |
files
|
| Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
changeset |
files
|
| Thu, 25 Aug 1994 10:47:33 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
changeset |
files
|
| Wed, 24 Aug 1994 18:49:29 +0200 |
lcp |
Subst/UTerm: updated for inductive defs; streamlined proofs
|
changeset |
files
|
| Mon, 22 Aug 1994 12:00:02 +0200 |
lcp |
HOL/ex/MT.thy: now mentions dependence upon Sum.thy
|
changeset |
files
|
| Mon, 22 Aug 1994 11:54:23 +0200 |
lcp |
new header & minor changes
|
changeset |
files
|
| Mon, 22 Aug 1994 11:02:35 +0200 |
lcp |
changed defn to def
|
changeset |
files
|
| Mon, 22 Aug 1994 10:56:45 +0200 |
lcp |
HOL/Sum.thy: generalized the type of Part
|
changeset |
files
|
| Fri, 19 Aug 1994 16:18:44 +0200 |
wenzelm |
replaced add_defns_i by add_defs_i;
|
changeset |
files
|
| Fri, 19 Aug 1994 11:27:19 +0200 |
lcp |
HOL/Trancl.thy: depends upon Prod
|
changeset |
files
|
| Fri, 19 Aug 1994 11:25:16 +0200 |
lcp |
HOL/Makefile, ROOT: updated for new .thy files
|
changeset |
files
|
| Fri, 19 Aug 1994 11:19:14 +0200 |
lcp |
HOL/Ord.thy,.ML: files now have header comments
|
changeset |
files
|
| Fri, 19 Aug 1994 11:15:01 +0200 |
lcp |
HOL/Sum: added disjoint sum of two sets as the plus operator, since + is
|
changeset |
files
|
| Fri, 19 Aug 1994 11:10:56 +0200 |
lcp |
HOL/subset.thy, equalities.thy, mono.thy: new
|
changeset |
files
|
| Fri, 19 Aug 1994 11:02:45 +0200 |
lcp |
HOL/fun.ML: renamed Fun.ML to avoid problems with MLs "fun" keyword
|
changeset |
files
|