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.
lcp [Tue, 28 Feb 1995 10:51:52 +0100] rev 918
Uses "suffix substitution" to shorten macro definitions.
lcp [Tue, 28 Feb 1995 10:50:37 +0100] rev 917
Re-organised to perform the tests independently. Now test
is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to
refer to the right command for running the object-logic. Uses "suffix
substitution" to shorten macro definitions.