Wed, 15 Mar 1995 10:56:39 +0100 Declares the function exit_use to behave like use but fail if
lcp [Wed, 15 Mar 1995 10:56:39 +0100] rev 955
Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
Wed, 15 Mar 1995 10:53:58 +0100 Now the "use" call has an exception handler, for prompt failure
lcp [Wed, 15 Mar 1995 10:53:58 +0100] rev 954
Now the "use" call has an exception handler, for prompt failure if errors are detected.
Wed, 15 Mar 1995 10:34:47 +0100 Now calls exit_use instead of use, for prompt failure if errors are detected.
lcp [Wed, 15 Mar 1995 10:34:47 +0100] rev 953
Now calls exit_use instead of use, for prompt failure if errors are detected.
Tue, 14 Mar 1995 10:40:04 +0100 Removed an old bug which made some simultaneous instantiations fail if they
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.
Tue, 14 Mar 1995 09:47:28 +0100 added exit 1
nipkow [Tue, 14 Mar 1995 09:47:28 +0100] rev 951
added exit 1
Mon, 13 Mar 1995 09:42:50 +0100 Removed superfluous type constraint
nipkow [Mon, 13 Mar 1995 09:42:50 +0100] rev 950
Removed superfluous type constraint
Mon, 13 Mar 1995 09:38:10 +0100 Changed treatment of during type inference internally generated type
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.
Sat, 11 Mar 1995 17:46:14 +0100 Added type constraints to enforce correct choice of variable names.
nipkow [Sat, 11 Mar 1995 17:46:14 +0100] rev 948
Added type constraints to enforce correct choice of variable names.
Sat, 11 Mar 1995 11:58:21 +0100 Put freeze into the signature TACTIC for export
lcp [Sat, 11 Mar 1995 11:58:21 +0100] rev 947
Put freeze into the signature TACTIC for export
Fri, 10 Mar 1995 10:20:18 +0100 Removed "localize"; instead, proofs refer to their own
lcp [Fri, 10 Mar 1995 10:20:18 +0100] rev 946
Removed "localize"; instead, proofs refer to their own assumptions.
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip