| 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
|
| Fri, 15 Jul 1994 13:53:18 +0200 |
nipkow |
added val eq_sym_conv = prover "(x=y) = (y=x)";
|
changeset |
files
|
| Tue, 12 Jul 1994 16:34:45 +0200 |
lcp |
fixed indentation
|
changeset |
files
|
| Fri, 08 Jul 1994 17:39:02 +0200 |
nipkow |
Integrated PL0.thy into PL.thy
|
changeset |
files
|
| Fri, 08 Jul 1994 17:22:58 +0200 |
nipkow |
Hidden dtK and Impossible with a "local" clause
|
changeset |
files
|
| Fri, 08 Jul 1994 12:01:55 +0200 |
clasohm |
added mixfix annotations to constructor declarations
|
changeset |
files
|
| Wed, 29 Jun 1994 12:04:04 +0200 |
clasohm |
added parentheses made necessary by change of constrain's precedence
|
changeset |
files
|
| Fri, 24 Jun 1994 15:11:39 +0200 |
lcp |
HOL/Nat/less_asym: renamed from less_anti_sym
|
changeset |
files
|
| Fri, 24 Jun 1994 15:10:13 +0200 |
lcp |
HOL/WF/wf_asym: renamed from wf_anti_sym
|
changeset |
files
|
| Mon, 20 Jun 1994 14:52:40 +0200 |
clasohm |
added prefix to name of induct axiom
|
changeset |
files
|
| Mon, 20 Jun 1994 12:05:03 +0200 |
nipkow |
Datatype -> Datatype.ML
|
changeset |
files
|
| Fri, 17 Jun 1994 18:34:12 +0200 |
lcp |
HOL/Arith/add_left_commute: tidied
|
changeset |
files
|
| Fri, 17 Jun 1994 18:32:25 +0200 |
lcp |
HOL/HOL.ML/notE: tidied the proof
|
changeset |
files
|
| Fri, 17 Jun 1994 18:30:18 +0200 |
lcp |
HOL/List/map_append,map_compose: new
|
changeset |
files
|
| Fri, 17 Jun 1994 18:28:36 +0200 |
lcp |
HOL/ex/NatSum: added another example
|
changeset |
files
|
| Fri, 17 Jun 1994 14:16:50 +0200 |
clasohm |
adopted to new datatype definition method
|
changeset |
files
|
| Fri, 17 Jun 1994 14:15:38 +0200 |
clasohm |
datatypes must now be defined using a thy file section
|
changeset |
files
|
| Wed, 15 Jun 1994 19:28:35 +0200 |
nipkow |
Added set comprehension as a syntactic abbreviation:
|
changeset |
files
|
| Wed, 01 Jun 1994 13:24:54 +0200 |
lcp |
added test for $ISABELLEBIN=source directory, to
|
changeset |
files
|
| Wed, 25 May 1994 13:03:19 +0200 |
lcp |
HOL/Arith: definition of diff now uses pred, not nat_rec
|
changeset |
files
|
| Wed, 25 May 1994 12:43:50 +0200 |
lcp |
HOL/equalities: added some identities from ZF/equalities
|
changeset |
files
|
| Wed, 25 May 1994 12:25:40 +0200 |
lcp |
HOL/HOL.ML/notE: tidied
|
changeset |
files
|
| Thu, 19 May 1994 17:07:19 +0200 |
wenzelm |
thy reader now initialised by init_thy_reader();
|
changeset |
files
|
| Fri, 13 May 1994 11:14:20 +0200 |
lcp |
HOL/Prod/pair_eq: renamed to Pair_fst_snd_eq
|
changeset |
files
|
| Tue, 03 May 1994 15:48:19 +0200 |
lcp |
removal of obsolete type-declaration syntax
|
changeset |
files
|
| Tue, 03 May 1994 11:30:09 +0200 |
lcp |
removal of obsolete type-declaration syntax
|
changeset |
files
|
| Sun, 24 Apr 1994 11:27:38 +0200 |
clasohm |
renamed theory files
isa94
|
changeset |
files
|
| Fri, 22 Apr 1994 21:23:14 +0200 |
clasohm |
renamed theory files
|
changeset |
files
|
| Thu, 21 Apr 1994 11:28:32 +0200 |
lcp |
tidied definitions and proofs
|
changeset |
files
|
| Thu, 21 Apr 1994 11:13:22 +0200 |
lcp |
HOL/arith.ML/plus_leD1: tidied
|
changeset |
files
|
| Tue, 19 Apr 1994 10:50:00 +0200 |
nipkow |
changed defns in hol.thy from = to ==
|
changeset |
files
|
| Wed, 06 Apr 1994 16:31:06 +0200 |
lcp |
Now simplifies before the induction
|
changeset |
files
|
| Wed, 30 Mar 1994 10:00:23 +0200 |
nipkow |
@ now associates to the right, just like #, in order to avoid loss of
|
changeset |
files
|
| Sun, 27 Mar 1994 16:43:06 +0200 |
nipkow |
Added some sums.
|
changeset |
files
|
| Sun, 27 Mar 1994 12:36:39 +0200 |
nipkow |
integrated permutative rewriting
|
changeset |
files
|
| Tue, 22 Mar 1994 19:55:29 +0100 |
nipkow |
used new field "simps" of Datatype
|
changeset |
files
|
| Tue, 22 Mar 1994 19:54:55 +0100 |
nipkow |
new field "simps" added
|
changeset |
files
|
| Tue, 22 Mar 1994 18:07:45 +0100 |
nipkow |
added dependency on datatype.ML
|
changeset |
files
|