src/FOL/simpdata.ML
changeset 4203 ca73de799b73
parent 4189 b8c7a6bc6c16
child 4325 e72cba5af6c5
equal deleted inserted replaced
4202:96876d71eef5 4203:ca73de799b73
   181 local val mktac = mk_case_split_inside_tac meta_iffD
   181 local val mktac = mk_case_split_inside_tac meta_iffD
   182 in
   182 in
   183 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
   183 fun split_inside_tac splits = mktac (map mk_meta_eq splits)
   184 end;
   184 end;
   185 
   185 
   186 val split_prem_tac = mk_case_split_prem_tac split_tac disjE conjE exE contrapos
   186 val split_asm_tac = mk_case_split_asm_tac split_tac 
   187 					    contrapos2 notnotD;
   187 			(disjE,conjE,exE,contrapos,contrapos2,notnotD);
   188 
   188 
   189 (*** Standard simpsets ***)
   189 (*** Standard simpsets ***)
   190 
   190 
   191 structure Induction = InductionFun(struct val spec=IFOL.spec end);
   191 structure Induction = InductionFun(struct val spec=IFOL.spec end);
   192 
   192