Mercurial Mercurial > hg > nominal2 / 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.
Nominal/ExTySch.thy
changeset 1605 d46a32cfcd89
parent 1599 8b5a1ad60487
child 1670 ed89a26b7074 
--- a/Nominal/ExTySch.thy	Tue Mar 23 09:34:32 2010 +0100
+++ b/Nominal/ExTySch.thy	Tue Mar 23 09:38:03 2010 +0100
@@ -86,10 +86,10 @@
     apply simp
     apply (rule allI)
     apply (rule allI)
-    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> TySch.All fset t) \<sharp>* pa)")
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (fset_to_set (fmap atom (p \<bullet> fset)))) \<sharp>* d \<and> supp (p \<bullet> All fset t) \<sharp>* pa)")
     apply clarify
-    apply(rule_tac t="p \<bullet> TySch.All fset t" and 
-                   s="pa \<bullet> (p \<bullet> TySch.All fset t)" in subst)
+    apply(rule_tac t="p \<bullet> All fset t" and 
+                   s="pa \<bullet> (p \<bullet> All fset t)" in subst)
     apply (rule supp_perm_eq)
     apply assumption
     apply (simp only: t_tyS.perm)
nominal2