| changeset 452 | 7ba2c16fe0c8 |
| parent 451 | 586e3dc4afdb |
| child 455 | 9cb45d022524 |
--- a/FSet.thy Sun Nov 29 08:48:06 2009 +0100 +++ b/FSet.thy Sun Nov 29 09:38:07 2009 +0100 @@ -469,6 +469,7 @@ apply (tactic {* (inj_repabs_tac_fset @{context}) 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 *}) apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) apply (rule IDENTITY_QUOTIENT) apply (rule FUN_QUOTIENT)