src/HOL/ex/SVC_Oracle.thy
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38864 4abe644fcea5
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -88,8 +88,8 @@
     1.4              else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
     1.5              else replace (c $ x $ y)   (*non-numeric comparison*)
     1.6      (*abstraction of a formula*)
     1.7 -    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.8 -      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.9 +    and fm ((c as Const(@{const_name HOL.conj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.10 +      | fm ((c as Const(@{const_name HOL.disj}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.11        | fm ((c as Const(@{const_name HOL.implies}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.12        | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
    1.13        | fm ((c as Const(@{const_name True}, _))) = c