author | nipkow |
Tue, 31 May 1994 13:17:41 +0200 | |
changeset 406 | 4d4e0442b106 |
parent 405 | c97514f63633 |
child 407 | 8039ac1065f7 |
--- a/src/Provers/simplifier.ML Sun May 29 15:14:28 1994 +0200 +++ b/src/Provers/simplifier.ML Tue May 31 13:17:41 1994 +0200 @@ -28,7 +28,7 @@ val simp_tac: simpset -> int -> tactic end; -structure Simplifier:SIMPLIFIER = +functor SimplifierFUN():SIMPLIFIER = struct datatype simpset = @@ -157,3 +157,5 @@ val simp_tac = gen_simp_tac (false,false); end; + +structure Simplifier = SimplifierFUN();