# HG changeset patch
# User haftmann
# Date 1256812897 -3600
# Node ID 74f0dcc0b5fb92680353b64c6c7f4ebc3ac41955
# Parent  ddd97d9dfbfbae93e328bda94a3d193c2f59e7af
moved algebraic classes to Ring_and_Field

diff -r ddd97d9dfbfb -r 74f0dcc0b5fb src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Thu Oct 29 11:41:36 2009 +0100
+++ b/src/HOL/Fact.thy	Thu Oct 29 11:41:37 2009 +0100
@@ -8,7 +8,7 @@
 header{*Factorial Function*}
 
 theory Fact
-imports Nat_Transfer
+imports Main
 begin
 
 class fact =
@@ -266,9 +266,6 @@
 lemma of_nat_fact_not_zero [simp]: "of_nat (fact n) \<noteq> (0::'a::semiring_char_0)"
 by auto
 
-class ordered_semiring_1 = ordered_semiring + semiring_1
-class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
-
 lemma of_nat_fact_gt_zero [simp]: "(0::'a::{ordered_semidom}) < of_nat(fact n)" by auto
 
 lemma of_nat_fact_ge_zero [simp]: "(0::'a::ordered_semidom) \<le> of_nat(fact n)"
diff -r ddd97d9dfbfb -r 74f0dcc0b5fb src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Oct 29 11:41:36 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Thu Oct 29 11:41:37 2009 +0100
@@ -767,6 +767,8 @@
 
 end
 
+class ordered_semiring_1 = ordered_semiring + semiring_1
+
 class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
   assumes mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
@@ -884,6 +886,8 @@
 
 end
 
+class ordered_semiring_1_strict = ordered_semiring_strict + semiring_1
+
 class mult_mono1 = times + zero + ord +
   assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
 
@@ -2025,15 +2029,15 @@
 
 lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
     ==> x * y <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
 
 lemma mult_left_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1
     ==> y * x <= x"
-by (auto simp add: mult_compare_simps);
+by (auto simp add: mult_compare_simps)
 
 lemma mult_imp_div_pos_le: "0 < (y::'a::ordered_field) ==> x <= z * y ==>
-    x / y <= z";
-by (subst pos_divide_le_eq, assumption+);
+    x / y <= z"
+by (subst pos_divide_le_eq, assumption+)
 
 lemma mult_imp_le_div_pos: "0 < (y::'a::ordered_field) ==> z * y <= x ==>
     z <= x / y"
@@ -2060,8 +2064,8 @@
 lemma frac_less: "(0::'a::ordered_field) <= x ==> 
     x < y ==> 0 < w ==> w <= z  ==> x / z < y / w"
   apply (rule mult_imp_div_pos_less)
-  apply simp;
-  apply (subst times_divide_eq_left);
+  apply simp
+  apply (subst times_divide_eq_left)
   apply (rule mult_imp_less_div_pos, assumption)
   apply (erule mult_less_le_imp_less)
   apply simp_all
@@ -2071,7 +2075,7 @@
     x <= y ==> 0 < w ==> w < z  ==> x / z < y / w"
   apply (rule mult_imp_div_pos_less)
   apply simp_all
-  apply (subst times_divide_eq_left);
+  apply (subst times_divide_eq_left)
   apply (rule mult_imp_less_div_pos, assumption)
   apply (erule mult_le_less_imp_less)
   apply simp_all