src/HOL/ex/SVC_Oracle.thy
changeset 25919 8b1c0d434824
parent 24470 41c81e23c08d
child 25929 6bfef23e26be
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Tue Jan 15 16:19:21 2008 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Tue Jan 15 16:19:23 2008 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4      (*abstraction of a numeric literal*)
     1.5      fun lit (t as Const(@{const_name HOL.zero}, _)) = t
     1.6        | lit (t as Const(@{const_name HOL.one}, _)) = t
     1.7 -      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
     1.8 +      | lit (t as Const(@{const_name Int.number_of}, _) $ w) = t
     1.9        | lit t = replace t
    1.10      (*abstraction of a real/rational expression*)
    1.11      fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)