src/HOL/ex/SVC_Oracle.thy
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Feb 19 14:47:01 2010 +0100
     1.3 @@ -63,21 +63,21 @@
     1.4      (*abstraction of a numeric literal*)
     1.5      fun lit t = if can HOLogic.dest_number t then t else replace t;
     1.6      (*abstraction of a real/rational expression*)
     1.7 -    fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.8 -      | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
     1.9 +    fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.10 +      | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.11        | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.12 -      | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.13 -      | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
    1.14 +      | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.15 +      | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
    1.16        | rat t = lit t
    1.17      (*abstraction of an integer expression: no div, mod*)
    1.18 -    fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.19 -      | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.20 -      | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.21 -      | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x)
    1.22 +    fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.23 +      | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.24 +      | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
    1.25 +      | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
    1.26        | int t = lit t
    1.27      (*abstraction of a natural number expression: no minus*)
    1.28 -    fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.29 -      | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.30 +    fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.31 +      | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
    1.32        | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
    1.33        | nat t = lit t
    1.34      (*abstraction of a relation: =, <, <=*)