clasohm [Fri, 17 Mar 1995 22:46:26 +0100] rev 964
fixed two severe bugs in calc_xrules and case_rule
nipkow [Fri, 17 Mar 1995 15:52:55 +0100] rev 963
Corrected a silly old bug in merge_tsigs.
Rewrote a lot of Nimmermann's code.
nipkow [Fri, 17 Mar 1995 15:49:37 +0100] rev 962
Added a few thms to nat_ss and list_ss
regensbu [Fri, 17 Mar 1995 15:35:09 +0100] rev 961
Removed bugs which occurred due to new generation mechanism for type variables
lcp [Thu, 16 Mar 1995 00:00:30 +0100] rev 960
Removed exception handlers, as they are now in ZF/Makefile.
clasohm [Wed, 15 Mar 1995 12:52:03 +0100] rev 959
removed print_msg parameter of infer_types
lcp [Wed, 15 Mar 1995 11:25:24 +0100] rev 958
Now mentions Coind
lcp [Wed, 15 Mar 1995 11:01:08 +0100] rev 957
Removed exception handlers, as they are now in ZF/Makefile.
lcp [Wed, 15 Mar 1995 10:59:20 +0100] rev 956
Now calls exit_use instead of use, for prompt failure if errors are detected.
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).
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.
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.
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