# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1266249766 -3600
# Node ID a6fc645be6e2c69de2d114054c2b67d2eccd4a62
# Parent  5650924c69ed71c162dc5ebdd807afdfb86c4b55# Parent  368ec514aa34f37b3f5da460cf6def32576fdfb2
merged

diff -r 5650924c69ed -r a6fc645be6e2 Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Mon Feb 15 17:02:26 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Mon Feb 15 17:02:46 2010 +0100
@@ -1,7 +1,7 @@
 
 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
 
-theory LarryInt 
+theory LarryInt
 imports Nat "../Quotient" "../Quotient_Product"
 begin
 
@@ -373,12 +373,14 @@
   "nat_raw"
 
 abbreviation
-  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"
+  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
 
 lemma nat_le_eq_zle_raw:
   shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
-apply(auto)
-sorry
+  apply (cases w)
+  apply (cases z)
+  apply (simp add: nat_raw_def le_raw_def)
+  by auto
 
 lemma [quot_respect]:
   shows "(intrel ===> op =) nat_raw nat_raw"