# HG changeset patch
# User haftmann
# Date 1266587220 -3600
# Node ID 3fd8c3edf6398ccd710c68fd65090cc9c50bc300
# Parent  f44ef0e2d178a7500339fb382a7d3fd3f1ad13dd
dropped reference to type classes

diff -r f44ef0e2d178 -r 3fd8c3edf639 src/HOL/Prolog/Func.thy
--- a/src/HOL/Prolog/Func.thy	Fri Feb 19 14:46:59 2010 +0100
+++ b/src/HOL/Prolog/Func.thy	Fri Feb 19 14:47:00 2010 +0100
@@ -10,31 +10,28 @@
 
 typedecl tm
 
-consts
-  abs     :: "(tm => tm) => tm"
-  app     :: "tm => tm => tm"
+axiomatization
+  abs     :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
+  app     :: "tm \<Rightarrow> tm \<Rightarrow> tm" and
 
-  cond    :: "tm => tm => tm => tm"
-  "fix"   :: "(tm => tm) => tm"
-
-  true    :: tm
-  false   :: tm
-  "and"   :: "tm => tm => tm"       (infixr "and" 999)
-  eq      :: "tm => tm => tm"       (infixr "eq" 999)
+  cond    :: "tm \<Rightarrow> tm \<Rightarrow> tm \<Rightarrow> tm" and
+  "fix"   :: "(tm \<Rightarrow> tm) \<Rightarrow> tm" and
 
-  Z       :: tm                     ("Z")
-  S       :: "tm => tm"
-(*
-        "++", "--",
-        "**"    :: tm => tm => tm       (infixr 999)
-*)
-        eval    :: "[tm, tm] => bool"
+  true    :: tm and
+  false   :: tm and
+  "and"   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixr "and" 999) and
+  eq      :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixr "eq" 999) and
+
+  Z       :: tm                     ("Z") and
+  S       :: "tm \<Rightarrow> tm" and
 
-instance tm :: plus ..
-instance tm :: minus ..
-instance tm :: times ..
+  plus    :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "+" 65) and
+  minus   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "-" 65) and
+  times   :: "tm \<Rightarrow> tm \<Rightarrow> tm"       (infixl "*" 70) and
 
-axioms   eval: "
+  eval    :: "tm \<Rightarrow> tm \<Rightarrow> bool" where
+
+eval: "
 
 eval (abs RR) (abs RR)..
 eval (app F X) V :- eval F (abs R) & eval X U & eval (R U) V..
@@ -59,7 +56,6 @@
 eval ( Z    * M) Z..
 eval ((S N) * M) K :- eval (N * M) L & eval (L + M) K"
 
-
 lemmas prog_Func = eval
 
 lemma "eval ((S (S Z)) + (S Z)) ?X"