src/HOL/ex/SVC_Oracle.thy
changeset 35084 e25eedfc15ce
parent 34974 18b41bba42b5
child 35092 cfe605c54e50
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 08:49:26 2010 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4      (*abstraction of a real/rational expression*)
     1.5      fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.6        | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.7 -      | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.8 +      | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.9        | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.10        | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
    1.11        | rat t = lit t