Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compiles
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 23 Mar 2010 09:38:03 +0100
changeset 1605 d46a32cfcd89
parent 1604 5ab97f43ec24
child 1606 75403378068b
compiles
Nominal/ExTySch.thy file | annotate | diff | comparison | revisions 
--- 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