src/HOL/ex/SVC_Oracle.thy
changeset 44064 5bce8ff0d9ae
parent 41460 ea56b98aee83
child 46218 ecf6375e2abb
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Mon Aug 08 08:55:49 2011 -0700
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Mon Aug 08 09:52:09 2011 -0700
     1.3 @@ -64,7 +64,7 @@
     1.4      (*abstraction of a real/rational expression*)
     1.5      fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.6        | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.7 -      | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.8 +      | rat ((c as Const(@{const_name Fields.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.9        | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.10        | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
    1.11        | rat t = lit t