diff -r 97f6e5c61f03 -r b16cac0b7c88 IntEx2.thy
--- a/IntEx2.thy	Sun Dec 06 23:35:02 2009 +0100
+++ b/IntEx2.thy	Mon Dec 07 00:03:12 2009 +0100
@@ -175,41 +175,41 @@
   fix i j k :: int
   show "(i + j) + k = i + (j + k)"
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *})
     done
   show "i + j = j + i" 
     unfolding add_int_def
-    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *})
     done
   show "0 + i = (i::int)"
     unfolding add_int_def Zero_int_def 
-    apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *})
     done
   show "- i + i = 0"
     unfolding add_int_def minus_int_def Zero_int_def 
-    apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *})
     done
   show "i - j = i + - j"
     by (simp add: diff_int_def)
   show "(i * j) * k = i * (j * k)"
     unfolding mult_int_def 
-    apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *})
     done
   show "i * j = j * i"
     unfolding mult_int_def 
-    apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *})
     done
   show "1 * i = i"
     unfolding mult_int_def One_int_def
-    apply(tactic {* lift_tac @{context} @{thm mult_one_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *})
     done
   show "(i + j) * k = i * k + j * k"
     unfolding mult_int_def add_int_def
-    apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *})
     done
   show "0 \<noteq> (1::int)"
     unfolding Zero_int_def One_int_def
-    apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *})
     done
 qed
 
@@ -246,21 +246,21 @@
   fix i j k :: int
   show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *})
     done
   show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
     by (auto simp add: less_int_def dest: antisym) 
   show "i \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *})
     done
   show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *})
     done
   show "i \<le> j \<or> j \<le> i"
     unfolding le_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *})
     done
 qed
 
@@ -289,7 +289,7 @@
   fix i j k :: int
   show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
     unfolding le_int_def add_int_def
-    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *})
     done
 qed
 
@@ -307,7 +307,7 @@
   fix i j k :: int
   show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
     unfolding mult_int_def le_int_def less_int_def Zero_int_def
-    apply(tactic {* lift_tac @{context} @{thm test} [@{thm int_equivp}] 1 *})
+    apply(tactic {* lift_tac @{context} @{thm test} 1 *})
     done
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: zabs_def)