Mercurial Mercurial > hg > tm2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Hoare_abc.thy
changeset 11 f8b2bf858caf
parent 0 1378b654acde 
--- a/thys/Hoare_abc.thy	Tue Mar 25 11:20:36 2014 +0000
+++ b/thys/Hoare_abc.thy	Thu Mar 27 11:50:37 2014 +0000
@@ -343,8 +343,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -527,8 +527,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -712,8 +712,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     apply (auto simp:sep_conj_ac fam_conj_simps)
     (***************************************************************************)
@@ -912,8 +912,8 @@
   ultimately show ?case 
     apply (rule_tac x = k in exI, rule_tac x = "{At ?e} \<union> ?elm_f sr" in exI)
     apply (unfold IA_def, intro condI, assumption+)
-    apply (rule_tac x = "?ks_f sr ks" in pred_exI)
-    apply (rule_tac x = "?idx_f sr ks ia" in pred_exI)
+    apply (rule_tac x = "?ks_f sr ks" in tm.pred_exI)
+    apply (rule_tac x = "?idx_f sr ks ia" in tm.pred_exI)
     apply (unfold fam_conj_disj_simp[OF fresh_atm])
     by (auto simp:sep_conj_ac fam_conj_simps)
 qed
tm2