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.
FSet.thy
changeset 459 020e27417b59
parent 458 44a70e69ef92
child 462 0911d3aabf47 
--- a/FSet.thy	Mon Nov 30 11:53:20 2009 +0100
+++ b/FSet.thy	Mon Nov 30 12:14:20 2009 +0100
@@ -505,20 +505,20 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply assumption
 apply (rule refl)
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
nominal2