nipkow [Sat, 11 Mar 1995 17:46:14 +0100] rev 948
Added type constraints to enforce correct choice of variable names.
lcp [Sat, 11 Mar 1995 11:58:21 +0100] rev 947
Put freeze into the signature TACTIC for export
lcp [Fri, 10 Mar 1995 10:20:18 +0100] rev 946
Removed "localize"; instead, proofs refer to their own
assumptions.
lcp [Thu, 09 Mar 1995 10:38:30 +0100] rev 945
Commented isof(c,t)
nipkow [Wed, 08 Mar 1995 17:23:07 +0100] rev 944
Added dependencies on ../Provers/hypsubst.ML and removed those on
../Provers/ind.ML
nipkow [Wed, 08 Mar 1995 14:35:26 +0100] rev 943
Replaced read by read_cterm.
nipkow [Wed, 08 Mar 1995 14:01:08 +0100] rev 942
Enforced partial evaluation of mk_case_split_tac.
nipkow [Wed, 08 Mar 1995 12:56:45 +0100] rev 941
Enforced partial evaluation of mk_case_split_tac
nipkow [Wed, 08 Mar 1995 12:37:59 +0100] rev 940
Added dependencies on files in Provers
nipkow [Wed, 08 Mar 1995 10:25:50 +0100] rev 939
Added pretty-printing coments
nipkow [Tue, 07 Mar 1995 15:00:34 +0100] rev 938
*** empty log message ***
nipkow [Tue, 07 Mar 1995 14:59:24 +0100] rev 937
*** empty log message ***
nipkow [Tue, 07 Mar 1995 14:57:37 +0100] rev 936
Hoare logic
lcp [Tue, 07 Mar 1995 13:37:48 +0100] rev 935
Changed Univ to Datatype in parents
lcp [Tue, 07 Mar 1995 13:34:33 +0100] rev 934
Replaced rules by defs. Also got rid of tyconstU by
including TyConst in the datatype's universe
lcp [Tue, 07 Mar 1995 13:32:22 +0100] rev 933
Replaced rules by defs
lcp [Tue, 07 Mar 1995 13:29:36 +0100] rev 932
Got rid of exvarU and constU by
including ExVar and Const in various datatype universes.
lcp [Tue, 07 Mar 1995 13:27:09 +0100] rev 931
Deleted constQU, exvarQU, expQU by including Const,
ExpVar, Exp in Value.thy's codatatype declaration.
lcp [Tue, 07 Mar 1995 13:21:38 +0100] rev 930
Replaced rules by defs
lcp [Tue, 07 Mar 1995 13:18:48 +0100] rev 929
Moved declarations of @QSUM and <*> to a syntax section.
Changed print_translation because <*> is now an infix.
lcp [Tue, 07 Mar 1995 13:15:25 +0100] rev 928
Moved declaration of ~= to a syntax section
clasohm [Fri, 03 Mar 1995 12:48:06 +0100] rev 927
replaced Pure by ProtoPure
clasohm [Fri, 03 Mar 1995 12:34:57 +0100] rev 926
fixed a bug in infer_types/exn_type_msg
clasohm [Fri, 03 Mar 1995 12:04:45 +0100] rev 925
new version of HOL/Integ with curried function application
clasohm [Fri, 03 Mar 1995 12:04:16 +0100] rev 924
new version of HOL/IMP with curried function application
clasohm [Fri, 03 Mar 1995 12:02:25 +0100] rev 923
new version of HOL with curried function application
clasohm [Fri, 03 Mar 1995 11:48:05 +0100] rev 922
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
wenzelm [Thu, 02 Mar 1995 12:07:20 +0100] rev 921
added declaration of syntactic const "_abs";
lcp [Tue, 28 Feb 1995 10:54:49 +0100] rev 920
Added initial /bin/csh line and comments
lcp [Tue, 28 Feb 1995 10:53:56 +0100] rev 919
No longer calls maketest; instead, the Makefile writes the file
test.