changeset 758 | 3104d62e7a16 |
parent 705 | f51c6069cd17 |
child 766 | df053507edba |
--- a/Quot/Examples/FSet.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/Examples/FSet.thy Thu Dec 17 14:58:33 2009 +0100 @@ -359,7 +359,7 @@ apply(regularize) apply(rule fun_rel_id_asm) apply(subst babs_simp) -apply(tactic {* quotient_tac @{context} 1 *}) +apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) apply(rule fun_rel_id_asm) apply(rule impI) apply(rule mp[OF eq_imp_rel[OF fset_equivp]])