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.