diff -r 1369c27c6966 -r a7de9d36f4f2 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Dec 19 00:13:25 2010 +0100
+++ b/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
@@ -130,21 +130,6 @@
 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
   "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
 
-lemma div_by_z3div:
-  "\<forall>k l. k div l = (
-    if k = 0 \<or> l = 0 then 0
-    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
-    else z3div (-k) (-l))"
-  by (auto simp add: z3div_def trigger_def)
-
-lemma mod_by_z3mod:
-  "\<forall>k l. k mod l = (
-    if l = 0 then k
-    else if k = 0 then 0
-    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
-    else - z3mod (-k) (-l))"
-  by (auto simp add: z3mod_def trigger_def)
-
 
 
 subsection {* Setup *}
@@ -391,8 +376,8 @@
 
 hide_type term_bool
 hide_type (open) pattern
-hide_const Pattern fun_app
-hide_const (open) trigger pat nopat weight z3div z3mod
+hide_const Pattern fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight