changeset 36717 | 2a72455be88b |
parent 36692 | 54b64d4ad524 |
parent 36701 | 787c33a0e468 |
child 36797 | cb074cec7a30 |
--- a/src/HOL/Tools/Qelim/cooper.ML Thu May 06 10:55:09 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Thu May 06 19:27:51 2010 +0200 @@ -3,7 +3,7 @@ *) signature COOPER = - sig +sig val cooper_conv : Proof.context -> conv exception COOPER of string * exn end; @@ -12,7 +12,6 @@ struct open Conv; -open Normalizer; exception COOPER of string * exn; fun simp_thms_conv ctxt =