avoiding direct references to numeral presentation
authorhaftmann
Mon Jan 21 08:43:29 2008 +0100 (2008-01-21)
changeset 259296bfef23e26be
parent 25928 042e877d9841
child 25930 83e3dd60affe
avoiding direct references to numeral presentation
src/HOL/ex/SVC_Oracle.thy
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Mon Jan 21 08:43:27 2008 +0100
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Mon Jan 21 08:43:29 2008 +0100
     1.3 @@ -62,10 +62,7 @@
     1.4                        SOME v => v
     1.5                      | NONE   => insert t)
     1.6      (*abstraction of a numeric literal*)
     1.7 -    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
     1.8 -      | lit (t as Const(@{const_name HOL.one}, _)) = t
     1.9 -      | lit (t as Const(@{const_name Int.number_of}, _) $ w) = t
    1.10 -      | lit t = replace t
    1.11 +    fun lit t = if can HOLogic.dest_number t then t else replace t;
    1.12      (*abstraction of a real/rational expression*)
    1.13      fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    1.14        | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)