changeset 387 | f78aa16daae5 |
parent 386 | 4fcbbb5b3b58 |
child 389 | d67240113f68 |
child 390 | 1dd6a21cdd1c |
--- a/FSet.thy Wed Nov 25 14:25:29 2009 +0100 +++ b/FSet.thy Wed Nov 25 15:20:10 2009 +0100 @@ -334,6 +334,8 @@ done lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" +apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *}) +apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) done