Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned op's
authornipkow
Wed, 20 Dec 2017 19:17:37 +0100
changeset 67230 b2800da9eb8a
parent 67229 4ecf0ef70efb
child 67231 754952c12293
tuned op's
src/HOL/Tools/groebner.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/groebner.ML	Wed Dec 20 14:53:34 2017 +0100
+++ b/src/HOL/Tools/groebner.ML	Wed Dec 20 19:17:37 2017 +0100
@@ -899,7 +899,7 @@
   | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm
   | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm
   | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm
-  | \<^term>\<open>op \<Longrightarrow>\<close> $_$_ => find_args bounds tm
+  | \<^term>\<open>Pure.imp\<close> $_$_ => find_args bounds tm
   | Const("op ==",_)$_$_ => find_args bounds tm  (* FIXME proper const name *)
   | \<^term>\<open>Trueprop\<close>$_ => find_term bounds (Thm.dest_arg tm)
   | _ => raise TERM ("find_term", []))
isabelle