src/ZF/Tools/datatype_package.ML
changeset 28839 32d498cf7595
parent 28678 d93980a6c3cb
child 28965 1de908189869
equal deleted 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