| 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
|
| Thu, 18 Aug 1994 12:48:03 +0200 |
lcp |
HOL/ex/Term, Simult: updated for new Split
|
changeset |
files
|
| Thu, 18 Aug 1994 12:42:19 +0200 |
lcp |
HOL/List: rotated arguments of List_case, list_case
|
changeset |
files
|
| Thu, 18 Aug 1994 12:38:12 +0200 |
lcp |
HOL/Prod: swapped args of split and simplified
|
changeset |
files
|
| Thu, 18 Aug 1994 12:23:52 +0200 |
lcp |
HOL/Univ: swapped args of split and simplified
|
changeset |
files
|
| Thu, 18 Aug 1994 12:13:26 +0200 |
lcp |
HOL/Sexp: rotated arguments of Sexp_case
|
changeset |
files
|
| Thu, 18 Aug 1994 12:07:51 +0200 |
lcp |
HOL/Nat: rotated arguments of nat_case; added translation for case macro
|
changeset |
files
|
| Thu, 18 Aug 1994 11:54:20 +0200 |
lcp |
HOL/Trancl: comp_cs is based upon prod_cs; tidied proofs
|
changeset |
files
|
| Thu, 18 Aug 1994 11:43:40 +0200 |
lcp |
HOL/Sum: rotated arguments of sum_case; added translation for case macro
|
changeset |
files
|
| Thu, 18 Aug 1994 11:40:54 +0200 |
lcp |
HOL/Subst/AList: swapped args of split and simplified
|
changeset |
files
|
| Thu, 18 Aug 1994 11:30:27 +0200 |
lcp |
HOL/LList: swapped args of split and simplified
|
changeset |
files
|
| Tue, 16 Aug 1994 09:57:51 +0200 |
nipkow |
allow long_id for reference to type in primrec.
|
changeset |
files
|
| Mon, 15 Aug 1994 15:20:34 +0200 |
nipkow |
Cleaned up code.
|
changeset |
files
|
| Sat, 13 Aug 1994 16:34:30 +0200 |
nipkow |
Used the new primitive recursive functions format for thy-files
|
changeset |
files
|
| Sat, 13 Aug 1994 16:33:53 +0200 |
nipkow |
Added primitive recursive functions (Norbert Voelker's code) to the datatype
|
changeset |
files
|
| Wed, 03 Aug 1994 11:00:40 +0200 |
nipkow |
renamed meta_obj_reflection meta_eq_to_obj_eq.
|
changeset |
files
|
| Tue, 02 Aug 1994 16:43:39 +0200 |
nipkow |
exposed meta_obj_reflection
|
changeset |
files
|
| Wed, 27 Jul 1994 19:08:40 +0200 |
lcp |
added a new example due to Robin Arthan
|
changeset |
files
|
| Thu, 21 Jul 1994 10:52:00 +0200 |
lcp |
HOL/Makefile: now test depends upon SUBST_FILES
|
changeset |
files
|
| Fri, 15 Jul 1994 14:04:28 +0200 |
nipkow |
Lots of simplifications
|
changeset |
files
|