# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256582130 -3600
# Node ID 9163c0f9830dd4f86b489a38d6243670dba7ec1e
# Parent  72165b83b9d62baa89c256ca708a1c972abb8f09
Simplifying Int.

diff -r 72165b83b9d6 -r 9163c0f9830d IntEx.thy
--- a/IntEx.thy	Mon Oct 26 15:32:17 2009 +0100
+++ b/IntEx.thy	Mon Oct 26 19:35:30 2009 +0100
@@ -169,10 +169,8 @@
 *}
 
 
-thm id_apply
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
-thm HOL.sym[OF lambda_prs_mn_b,simplified]
 
 ML {*
   fun simp_lam_prs lthy thm =
@@ -183,19 +181,19 @@
 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
 
 ML {*
-  fun simp_allex_prs lthy thm =
+  fun simp_allex_prs lthy quot thm =
     let
-      val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]};
+      val rwf = @{thm FORALL_PRS} OF [quot];
       val rwfs = @{thm "HOL.sym"} OF [rwf];
-      val rwe = @{thm EXISTS_PRS[OF QUOTIENT_my_int]};
+      val rwe = @{thm EXISTS_PRS} OF [quot];
       val rwes = @{thm "HOL.sym"} OF [rwe]
     in
-      (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm))
+      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
     end
     handle _ => thm
 *}
 
-ML {* val t_a = simp_allex_prs @{context} t_l *}
+ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 
 ML {* val t_defs = @{thms PLUS_def} *}
 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}