equal
deleted
inserted
replaced
906 |
906 |
907 ML {* |
907 ML {* |
908 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
908 fun fs_tac induct supports = ind_tac induct THEN_ALL_NEW ( |
909 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
909 rtac @{thm supports_finite} THEN' resolve_tac supports) THEN_ALL_NEW |
910 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
910 asm_full_simp_tac (HOL_ss addsimps @{thms supp_atom supp_atom_image supp_fset_to_set |
911 supp_fmap_atom finite_insert finite.emptyI finite_Un}) |
911 supp_fmap_atom finite_insert finite.emptyI finite_Un finite_supp}) |
912 *} |
912 *} |
913 |
913 |
914 ML {* |
914 ML {* |
915 fun prove_fs ctxt induct supports tys = |
915 fun prove_fs ctxt induct supports tys = |
916 let |
916 let |