temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
authorhuffman
Thu, 31 May 2012 10:01:15 +0200
changeset 48047 2efdcc7d0775
parent 48046 359bec38a4ee
child 48048 87b94fb75198
temporarily comment out portion of Quotient_Examples/Quotient_Rat.thy, broken by changes to Int.thy
src/HOL/Quotient_Examples/Quotient_Rat.thy
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy	Wed May 30 18:09:23 2012 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy	Thu May 31 10:01:15 2012 +0200
@@ -114,6 +114,8 @@
 
 lemmas [simp] = Respects_def
 
+(* FIXME: (partiality_)descending raises exception TYPE_MATCH
+
 instantiation rat :: comm_ring_1
 begin
 
@@ -260,5 +262,6 @@
     then show "\<exists>z\<Colon>int. a * b \<le> z * b * b" by auto
   qed
 qed
+*)
 
 end