# HG changeset patch # User haftmann # Date 1230906911 -3600 # Node ID 88d23c927e3791ea59239e2e377e350c750e9729 # Parent 2c764235e041cb27d88f985de238bc81c7f228fd# Parent 3eb95594ba89af72a92731c7214ef69d8b09c973 merged diff -r 2c764235e041 -r 88d23c927e37 src/HOL/Rational.thy --- a/src/HOL/Rational.thy Fri Jan 02 11:31:40 2009 +0100 +++ b/src/HOL/Rational.thy Fri Jan 02 15:35:11 2009 +0100 @@ -851,7 +851,7 @@ definition Fract_norm :: "int \ int \ rat" where [simp, code del]: "Fract_norm a b = Fract a b" -lemma [code]: "Fract_norm a b = (if a = 0 \ b = 0 then 0 else let c = zgcd a b in +lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \ 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 \ d = 0 else if d = 0 then a = 0 \ 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 2c764235e041 -r 88d23c927e37 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Jan 02 11:31:40 2009 +0100 +++ b/src/Pure/Isar/ROOT.ML Fri Jan 02 15:35:11 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 2c764235e041 -r 88d23c927e37 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Jan 02 11:31:40 2009 +0100 +++ b/src/Pure/Isar/class.ML Fri Jan 02 15:35:11 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;