src/HOL/ex/SVC_Oracle.thy
changeset 38558 32ad17fe2b9c
parent 38549 d0385f2764d8
child 38786 e46e7a9cb622
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -91,15 +91,15 @@
     1.4      and fm ((c as Const(@{const_name "op &"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.5        | fm ((c as Const(@{const_name "op |"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.6        | fm ((c as Const(@{const_name "op -->"}, _)) $ p $ q) = c $ (fm p) $ (fm q)
     1.7 -      | fm ((c as Const(@{const_name "Not"}, _)) $ p) = c $ (fm p)
     1.8 -      | fm ((c as Const(@{const_name "True"}, _))) = c
     1.9 -      | fm ((c as Const(@{const_name "False"}, _))) = c
    1.10 +      | fm ((c as Const(@{const_name Not}, _)) $ p) = c $ (fm p)
    1.11 +      | fm ((c as Const(@{const_name True}, _))) = c
    1.12 +      | fm ((c as Const(@{const_name False}, _))) = c
    1.13        | fm (t as Const(@{const_name "op ="},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.14        | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.15        | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    1.16        | fm t = replace t
    1.17      (*entry point, and abstraction of a meta-formula*)
    1.18 -    fun mt ((c as Const(@{const_name "Trueprop"}, _)) $ p) = c $ (fm p)
    1.19 +    fun mt ((c as Const(@{const_name Trueprop}, _)) $ p) = c $ (fm p)
    1.20        | mt ((c as Const("==>", _)) $ p $ q)  = c $ (mt p) $ (mt q)
    1.21        | mt t = fm t  (*it might be a formula*)
    1.22    in (list_all (params, mt body), !pairs) end;