src/HOL/ex/SVC_Oracle.thy
changeset 38786 e46e7a9cb622
parent 38558 32ad17fe2b9c
child 38795 848be46708dc
--- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 13:44:50 2010 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 26 20:51:17 2010 +0200
@@ -90,7 +90,7 @@
     (*abstraction of a formula*)
     and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
-      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
+      | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
       | fm ((c as Const(@{const_name True}, _))) = c
       | fm ((c as Const(@{const_name False}, _))) = c