tuned

--- a/src/HOL/Library/ExecutableRat.thy	Sat May 19 11:33:24 2007 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Sat May 19 11:33:25 2007 +0200
@@ -10,7 +10,7 @@
 begin
 
 text {*
-  Actually \emph{nothing} is proved about the implementation.
+  Actually \emph{nothing} is proved about this implementation.
 *}
 
 subsection {* Representation and operations of executable rationals *}
@@ -111,13 +111,11 @@
 code_modulename OCaml
   ExecutableRat Rational
 
+code_modulename Haskell
+  ExecutableRat Rational
 
 subsubsection {* rat as abstype *}
 
-lemma [code func]: -- {* prevents eq constraint *}
-  shows "All = All"
-    and "contents = contents" by rule+
-
 code_const div_zero
   (SML "raise/ Fail/ \"Division by zero\"")
   (OCaml "failwith \"Division by zero\"")

--- a/src/HOL/Real/ferrante_rackoff_proof.ML	Sat May 19 11:33:24 2007 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Sat May 19 11:33:25 2007 +0200
@@ -13,17 +13,18 @@
 struct
 
     (* Some certified types *)
-val cbT = ctyp_of (the_context()) HOLogic.boolT;
-val rT = Type("RealDef.real",[]);
-val crT = ctyp_of (the_context()) (Type("RealDef.real",[]));
-    (* Normalization*)
+val cbT = @{ctyp bool};
+val rT = @{typ RealDef.real};
+val crT = @{ctyp RealDef.real};
+
+(* Normalization*)
 
 
         (* Computation of uset *)
 fun uset x fm = 
     case fm of
-        Const("op &",_)$p$q => (uset x p) union (uset x q)
-      | Const("op |",_)$p$q => (uset x p) union (uset x q)
+        Const("op &",_)$p$q => fold (insert (op =)) (uset x p) (uset x q)
+      | Const("op |",_)$p$q => fold (insert (op =)) (uset x p) (uset x q)
       | Const(@{const_name Orderings.less},_)$s$t => if s=x then [t] 
                                else if t = x then [s]
                                else []
@@ -35,9 +36,12 @@
       | Const("Not",_)$ (Const("op =",_)$s$t) => if s=x then [t] 
                                                  else []
       | _ => [];
-val rsT = Type("set",[rT]);
-fun holrealset [] = Const("{}",rsT)
-  | holrealset (x::xs) = Const("insert",[rT,rsT] ---> rsT)$x$(holrealset xs);
+
+val rsT = @{typ "RealDef.real set"};
+
+fun holrealset [] = @{term "{} :: RealDef.real set"}
+  | holrealset (x::xs) = @{term "insert :: RealDef.real => RealDef.real set => RealDef.real set"}
+      $ x $ holrealset xs;
 fun prove_bysimp thy ss t = Goal.prove (ProofContext.init thy) [] [] 
                        (HOLogic.mk_Trueprop t) (fn _ => simp_tac ss 1);