Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/cooper_tac.ML
changeset 56245 84fc7dfa3cd4
parent 55987 52c22561996d
child 57514 bdc2c6b40bf2 
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 15:12:03 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Fri Mar 21 20:33:56 2014 +0100
@@ -84,7 +84,7 @@
     (* The result of the quantifier elimination *)
     val (th, tac) =
       (case (prop_of pre_thm) of
-        Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
+        Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
           let
             val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
           in
isabelle