equal
deleted
inserted
replaced
1352 end; |
1352 end; |
1353 |
1353 |
1354 val cTs = map (SOME o certifyT lthy o TFree) induct_params; |
1354 val cTs = map (SOME o certifyT lthy o TFree) induct_params; |
1355 |
1355 |
1356 val weak_ctor_induct_thms = |
1356 val weak_ctor_induct_thms = |
1357 let fun insts i = (replicate (i - 1) TrueI) @ (@{thm asm_rl} :: replicate (n - i) TrueI); |
1357 let fun insts i = (replicate (i - 1) TrueI) @ (asm_rl :: replicate (n - i) TrueI); |
1358 in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end; |
1358 in map (fn i => (ctor_induct_thm OF insts i) RS mk_conjunctN n i) ks end; |
1359 |
1359 |
1360 val (ctor_induct2_thm, induct2_params) = |
1360 val (ctor_induct2_thm, induct2_params) = |
1361 let |
1361 let |
1362 fun mk_prem phi ctor ctor' sets sets' x y = |
1362 fun mk_prem phi ctor ctor' sets sets' x y = |