src/HOL/HOLCF/IOA/NTP/Impl.thy

   ML_prf {* val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}]) *}
 
   txt {* 10 - 7 *}
   apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
   txt {* 6 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
 
   txt {* 6 - 5 *}
   apply (tactic "EVERY1 [tac2,tac2]")
 
   txt {* 4 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   apply (tactic "tac2 1")
 
   txt {* 3 *}
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
     (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}]
+  apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
     (@{thm Impl.hdr_sum_def})] *})
   apply arith
 
   txt {* 2 *}
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
   apply (intro strip)
   apply (erule conjE)+
   apply simp
 
   txt {* 1 *}
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv1_def}]
                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (intro strip)
   apply (erule conjE)+
-  apply (tactic {* fold_goals_tac [rewrite_rule [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic {* fold_goals_tac @{context}
+    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
   apply simp
 
   done
 
 

   apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1")
   apply (simp (no_asm) add: inv3_def)
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
   apply (erule conjE)+
   apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
     k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm inv1_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm inv1_def}]
                                 (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
   apply (simp add: hdr_sum_def Multiset.count_def)
   apply (rule add_le_mono)
   apply (rule countm_props)
   apply (simp (no_asm))

   txt {* 1 *}
   apply (tactic "tac3 1")
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
     (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
   done
 
 

   apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
 
   txt {* 2 b *}
 
   apply (intro strip, (erule conjE)+)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
   apply simp
 
   txt {* 1 *}
   apply (tactic "tac4 1")
   apply (intro strip, (erule conjE)+)
   apply (rule ccontr)
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv2_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv2_def}]
                                (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
-  apply (tactic {* forward_tac [rewrite_rule [@{thm Impl.inv3_def}]
+  apply (tactic {* forward_tac [rewrite_rule @{context} [@{thm Impl.inv3_def}]
                                (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
   apply simp
   apply (erule_tac x = "m" in allE)
   apply simp
   done