tuned;

--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -3,12 +3,12 @@
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Construction of hyperreals using ultrafilters
-*) 
+*)
 
 HyperDef = Filter + Real +
 
-consts 
- 
+consts
+
     FreeUltrafilterNat   :: nat set set    ("\\<U>")
 
 defs
@@ -19,10 +19,10 @@
 
 constdefs
     hyprel :: "((nat=>real)*(nat=>real)) set"
-    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
+    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) &
                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
 
-typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
+typedef hypreal = "UNIV//hyprel"   (quotient_def)
 
 instance
    hypreal  :: {ord, zero, one, plus, times, minus, inverse}
@@ -38,24 +38,24 @@
   hypreal_minus_def
   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
 
-  hypreal_diff_def 
+  hypreal_diff_def
   "x - y == x + -(y::hypreal)"
 
   hypreal_inverse_def
-  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
+  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
                     hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
 
   hypreal_divide_def
   "P / Q::hypreal == P * inverse Q"
-  
+
 constdefs
 
-  hypreal_of_real  :: real => hypreal                 
+  hypreal_of_real  :: real => hypreal
   "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
 
   omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
   "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
-    
+
   epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
   "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
 
@@ -63,24 +63,22 @@
   omega   :: hypreal   ("\\<omega>")
   epsilon :: hypreal   ("\\<epsilon>")
 
-  
-defs 
 
-  hypreal_add_def  
+defs
+
+  hypreal_add_def
   "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
                 hyprel``{%n::nat. X n + Y n})"
 
-  hypreal_mult_def  
+  hypreal_mult_def
   "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
                 hyprel``{%n::nat. X n * Y n})"
 
   hypreal_less_def
-  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
-                               Y: Rep_hypreal(Q) & 
+  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &
+                               Y: Rep_hypreal(Q) &
                                {n::nat. X n < Y n} : FreeUltrafilterNat"
   hypreal_le_def
-  "P <= (Q::hypreal) == ~(Q < P)" 
+  "P <= (Q::hypreal) == ~(Q < P)"
 
 end
- 
-

--- a/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -12,13 +12,13 @@
     "hypnatrel == {p. EX X Y. p = ((X::nat=>nat),Y) & 
                        {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}"
 
-typedef hypnat = "UNIV//hypnatrel"              (Equiv.quotient_def)
+typedef hypnat = "UNIV//hypnatrel"              (quotient_def)
 
 instance
    hypnat  :: {ord, zero, one, plus, times, minus}
 
 consts
-  "whn"       :: hypnat               ("whn")  
+  whn       :: hypnat
 
 constdefs
 

--- a/src/HOL/Integ/IntDef.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -12,7 +12,7 @@
   "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Integ)
-  int = "UNIV//intrel"            (Equiv.quotient_def)
+  int = "UNIV//intrel"            (quotient_def)
 
 instance
   int :: {ord, zero, one, plus, times, minus}

--- a/src/HOL/Real/PRat.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Real/PRat.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -11,7 +11,7 @@
     ratrel   ::  "((pnat * pnat) * (pnat * pnat)) set"
     "ratrel  ==  {p. ? x1 y1 x2 y2. p=((x1::pnat,y1),(x2,y2)) & x1*y2 = x2*y1}" 
 
-typedef prat = "UNIV//ratrel"          (Equiv.quotient_def)
+typedef prat = "UNIV//ratrel"          (quotient_def)
 
 instance
    prat  :: {ord,plus,times}

--- a/src/HOL/Real/RealDef.thy	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Aug 08 23:52:55 2002 +0200
@@ -15,7 +15,7 @@
   "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
 
 typedef (REAL)
-  real = "UNIV//realrel"  (Equiv.quotient_def)
+  real = "UNIV//realrel"  (quotient_def)
 
 
 instance

--- a/src/ZF/arith_data.ML	Thu Aug 08 23:51:24 2002 +0200
+++ b/src/ZF/arith_data.ML	Thu Aug 08 23:52:55 2002 +0200
@@ -13,7 +13,7 @@
   (*tools for use in similar applications*)
   val gen_trans_tac: thm -> thm option -> tactic
   val prove_conv: string -> tactic list -> Sign.sg ->
-                  thm list -> term * term -> thm option
+                  thm list -> string list -> term * term -> thm option
   val simplify_meta_eq: thm list -> thm -> thm
   (*debugging*)
   structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
@@ -68,13 +68,13 @@
 
 fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
 
-fun prove_conv name tacs sg hyps (t,u) =
+fun prove_conv name tacs sg hyps xs (t,u) =
   if t aconv u then None
   else
   let val hyps' = filter (not o is_eq_thm) hyps
       val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
-  in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
+  in Some (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
       handle ERROR_MESSAGE msg =>
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
   end;