--- a/src/HOL/Rat.thy Tue Mar 31 16:49:41 2015 +0100
+++ b/src/HOL/Rat.thy Tue Mar 31 21:54:32 2015 +0200
@@ -101,7 +101,7 @@
shows "P q"
using assms by (cases q) simp
-instantiation rat :: field_inverse_zero
+instantiation rat :: field
begin
lift_definition zero_rat :: "rat" is "(0, 1)"
@@ -441,7 +441,7 @@
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff)
-instantiation rat :: linordered_field_inverse_zero
+instantiation rat :: linordered_field
begin
definition
@@ -689,7 +689,7 @@
done
lemma of_rat_inverse:
- "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
+ "(of_rat (inverse a)::'a::{field_char_0, field}) =
inverse (of_rat a)"
by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
@@ -698,7 +698,7 @@
by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
lemma of_rat_divide:
- "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
+ "(of_rat (a / b)::'a::{field_char_0, field})
= of_rat a / of_rat b"
by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
@@ -875,7 +875,7 @@
done
lemma Rats_inverse [simp]:
- fixes a :: "'a::{field_char_0, field_inverse_zero}"
+ fixes a :: "'a::{field_char_0, field}"
shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)
@@ -891,7 +891,7 @@
done
lemma Rats_divide [simp]:
- fixes a b :: "'a::{field_char_0, field_inverse_zero}"
+ fixes a b :: "'a::{field_char_0, field}"
shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
apply (auto simp add: Rats_def)
apply (rule range_eqI)