# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266249152 -3600
# Node ID 368ec514aa34f37b3f5da460cf6def32576fdfb2
# Parent  fbaebf08c1bd6717b256b2e305bce24c498a1e2a# Parent  2ad8e66de294b85cd4f59eeade71139daafe02d7
merge

diff -r fbaebf08c1bd -r 368ec514aa34 Quot/Examples/LarryInt.thy
--- a/Quot/Examples/LarryInt.thy	Mon Feb 15 16:50:11 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Mon Feb 15 16:52:32 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"