src/HOL/ex/SVC_Oracle.thy
changeset 38549 d0385f2764d8
parent 36176 3fe7e97ccca8
child 38558 32ad17fe2b9c
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 10:27:12 2010 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 11:02:14 2010 +0200
     1.3 @@ -88,18 +88,18 @@
     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("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.8 -      | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.9 -      | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.10 -      | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
    1.11 -      | fm ((c as Const("True", _))) = c
    1.12 -      | fm ((c as Const("False", _))) = c
    1.13 -      | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.14 +    and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.15 +      | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.16 +      | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
    1.17 +      | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
    1.18 +      | fm ((c as Const(@{const_name "True"}, _))) = c
    1.19 +      | fm ((c as Const(@{const_name "False"}, _))) = c
    1.20 +      | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.21        | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.22        | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.23        | fm t = replace t
    1.24      (*entry point, and abstraction of a meta-formula*)
    1.25 -    fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    1.26 +    fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
    1.27        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    1.28        | mt t = fm t  (*it might be a formula*)
    1.29    in (list_all (params, mt body), !pairs) end;