# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260431041 -3600
# Node ID cc3c55f56116757baf6a6faf0e276a3d6392fb5b
# Parent  d5c888ec56c79cb486d9449f51ad3837db6d2c9b
Removed 'Presburger' as it introduces int & other minor cleaning in Int2.

diff -r d5c888ec56c7 -r cc3c55f56116 Quot/Examples/IntEx2.thy
--- a/Quot/Examples/IntEx2.thy	Thu Dec 10 05:11:53 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Thu Dec 10 08:44:01 2009 +0100
@@ -1,5 +1,5 @@
 theory IntEx2
-imports "../QuotMain" Nat Presburger
+imports "../QuotMain" Nat
 (*uses
   ("Tools/numeral.ML")
   ("Tools/numeral_syntax.ML")
@@ -89,7 +89,7 @@
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
 by auto
 
-lemma minus_raw_rsp[quot_respect]:
+lemma uminus_raw_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx>) uminus_raw uminus_raw"
   by auto
 
@@ -172,10 +172,6 @@
 
 text{* The integers form a @{text comm_ring_1}*}
 
-ML {* qconsts_lookup @{theory} @{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} *}
-ML {* dest_Type (snd (dest_Const @{term "0 :: int"})) *}
-ML {* @{term "0 :: int"} *}
-
 instance int :: comm_ring_1
 proof
   fix i j k :: int