src/ZF/Tools/datatype_package.ML
 changeset 28839 32d498cf7595 parent 28678 d93980a6c3cb child 28965 1de908189869
equal inserted replaced
28838:d5db6dfcb34a 28839:32d498cf7595
`   289   fun prove_case_eqn (arg, con_def) =`
`   289   fun prove_case_eqn (arg, con_def) =`
`   290     Goal.prove_global thy1 [] []`
`   290     Goal.prove_global thy1 [] []`
`   291       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))`
`   291       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))`
`   292       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)`
`   292       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)`
`   293       (fn _ => EVERY`
`   293       (fn _ => EVERY`
`   294         [rewtac con_def,`
`   294         [rewrite_goals_tac [con_def],`
`   295          rtac case_trans 1,`
`   295          rtac case_trans 1,`
`   296          REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);`
`   296          REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);`
`   297 `
`   297 `
`   298   val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);`
`   298   val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);`
`   299 `
`   299 `