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.
LFex.thy
changeset 446 84ee3973f083
parent 445 f1c0a66284d3
child 450 2dc708ddb93a 
--- a/LFex.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/LFex.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -297,7 +297,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -317,14 +317,14 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -347,18 +347,18 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -375,28 +375,28 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -416,10 +416,10 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -445,21 +445,21 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 done
 
 print_quotients
nominal2