changeset 37117 | 59cee8807c29 |
parent 36945 | 9bec62c10714 |
child 37388 | 793618618f78 |
--- a/src/HOL/Tools/Qelim/cooper.ML Tue May 25 20:22:55 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue May 25 20:28:16 2010 +0200 @@ -10,6 +10,7 @@ val get: Proof.context -> entry val del: term list -> attribute val add: term list -> attribute + exception COOPER of string val conv: Proof.context -> conv val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic val method: (Proof.context -> Method.method) context_parser