nipkow [Tue, 14 Mar 1995 10:40:04 +0100] rev 952
Removed an old bug which made some simultaneous instantiations fail if they
were given in the "wrong" order.
Rewrote sign/infer_types.
Fixed some comments.
nipkow [Tue, 14 Mar 1995 09:47:28 +0100] rev 951
added exit 1
nipkow [Mon, 13 Mar 1995 09:42:50 +0100] rev 950
Removed superfluous type constraint
nipkow [Mon, 13 Mar 1995 09:38:10 +0100] rev 949
Changed treatment of during type inference internally generated type
variables.
1. They are renamed to 'a, 'b, 'c etc away from a given set of used names.
2. They are either frozen (turned into TFrees) or left schematic (TVars)
depending on a parameter. In goals they are frozen, for instantiations they
are left schematic.
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