# HG changeset patch
# User haftmann
# Date 1230880524 -3600
# Node ID 3eb95594ba89af72a92731c7214ef69d8b09c973
# Parent  5c71a6da989d04b1f7d0bab4bc4df73eed8d3dbc# Parent  496b94152b55d35aa0200419057742d899b55789
merged

diff -r 5c71a6da989d -r 3eb95594ba89 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Fri Jan 02 00:21:59 2009 +0100
+++ b/src/HOL/Rational.thy	Fri Jan 02 08:15:24 2009 +0100
@@ -851,7 +851,7 @@
 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
   [simp, code del]: "Fract_norm a b = Fract a b"
 
-lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
+lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
   if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
   by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
 
@@ -871,7 +871,7 @@
        then c = 0 \<or> d = 0
      else if d = 0
        then a = 0 \<or> b = 0
-     else a * d =  b * c)"
+     else a * d = b * c)"
   by (auto simp add: eq eq_rat)
 
 lemma rat_eq_refl [code nbe]:
diff -r 5c71a6da989d -r 3eb95594ba89 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jan 02 00:21:59 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML	Fri Jan 02 08:15:24 2009 +0100
@@ -55,9 +55,9 @@
 use "overloading.ML";
 use "locale.ML";
 use "new_locale.ML";
-use "expression.ML";
 use "class.ML";
 use "theory_target.ML";
+use "expression.ML";
 use "instance.ML";
 use "subclass.ML";
 
diff -r 5c71a6da989d -r 3eb95594ba89 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jan 02 00:21:59 2009 +0100
+++ b/src/Pure/Isar/class.ML	Fri Jan 02 08:15:24 2009 +0100
@@ -85,7 +85,7 @@
 
 end;
 
-structure New_Locale =
+(*structure New_Locale =
 struct
 
 val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
@@ -106,7 +106,7 @@
 val parameters_of = NewLocale.params_of; (*why typ option?*)
 val add_locale = Expression.add_locale;
 
-end;
+end;*)
 
 structure Locale = Old_Locale;