Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/svc_oracle.ML
changeset 22997 d4f3b015b50b
parent 20817 7ec9b692183c
child 23881 851c74f1bb69 
--- a/src/HOL/ex/svc_oracle.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/ex/svc_oracle.ML	Thu May 17 19:49:40 2007 +0200
@@ -41,27 +41,27 @@
                       SOME v => v
                     | NONE   => insert t)
     (*abstraction of a numeric literal*)
-    fun lit (t as Const("0", _)) = t
-      | lit (t as Const("1", _)) = t
-      | lit (t as Const("Numeral.number_of", _) $ w) = t
+    fun lit (t as Const(@{const_name HOL.zero}, _)) = t
+      | lit (t as Const(@{const_name HOL.one}, _)) = t
+      | lit (t as Const(@{const_name Numeral.number_of}, _) $ w) = t
       | lit t = replace t
     (*abstraction of a real/rational expression*)
-    fun rat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.minus", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.divide", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.times", _)) $ x $ y) = c $ (rat x) $ (rat y)
-      | rat ((c as Const("HOL.uminus", _)) $ x) = c $ (rat x)
+    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
+      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
       | rat t = lit t
     (*abstraction of an integer expression: no div, mod*)
-    fun int ((c as Const("HOL.plus", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.minus", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.times", _)) $ x $ y) = c $ (int x) $ (int y)
-      | int ((c as Const("HOL.uminus", _)) $ x) = c $ (int x)
+    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
+      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
       | int t = lit t
     (*abstraction of a natural number expression: no minus*)
-    fun nat ((c as Const("HOL.plus", _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const("HOL.times", _)) $ x $ y) = c $ (nat x) $ (nat y)
-      | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
+    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
+      | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
       | nat t = lit t
     (*abstraction of a relation: =, <, <=*)
     fun rel (T, c $ x $ y) =
@@ -78,8 +78,8 @@
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("Orderings.less",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const("Orderings.less_eq", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
isabelle