paulson [Thu, 05 Sep 1996 18:31:14 +0200] rev 1957
Now uses thin_tac
paulson [Thu, 05 Sep 1996 18:30:13 +0200] rev 1956
Renaming of _rews to _simps
paulson [Thu, 05 Sep 1996 18:29:43 +0200] rev 1955
Added thin_tac to signature; previous change was useless
paulson [Thu, 05 Sep 1996 18:28:54 +0200] rev 1954
Some renaming. Note that this miniscoping is more
general than that of ../simpdata.ML, as distributive laws are included.
On this other hand this version is for NNF only.
paulson [Thu, 05 Sep 1996 18:28:01 +0200] rev 1953
Introduction of miniscoping for FOL
paulson [Thu, 05 Sep 1996 10:30:42 +0200] rev 1952
Pretty-printing change to emphasize the scope of assumptions
paulson [Thu, 05 Sep 1996 10:29:52 +0200] rev 1951
Declared thin_tac
paulson [Thu, 05 Sep 1996 10:29:20 +0200] rev 1950
Miniscoping rules are deleted, as these brittle proofs
would otherwise have to be entirely redone
paulson [Thu, 05 Sep 1996 10:27:36 +0200] rev 1949
Simplified some proofs for compatibility with miniscoping
paulson [Thu, 05 Sep 1996 10:23:55 +0200] rev 1948
Added miniscoping to the simplifier: quantifiers are now pushed in