equal
deleted
inserted
replaced
1489 *} |
1489 *} |
1490 |
1490 |
1491 setup {* |
1491 setup {* |
1492 Induct.setup #> |
1492 Induct.setup #> |
1493 Context.theory_map (Induct.map_simpset (fn ss => ss |
1493 Context.theory_map (Induct.map_simpset (fn ss => ss |
1494 setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #> |
1494 setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #> |
1495 map (Simplifier.rewrite_rule (map Thm.symmetric |
1495 map (Simplifier.rewrite_rule (map Thm.symmetric |
1496 @{thms induct_rulify_fallback induct_true_def induct_false_def}))) |
1496 @{thms induct_rulify_fallback induct_true_def induct_false_def}))) |
1497 addsimprocs |
1497 addsimprocs |
1498 [Simplifier.simproc @{theory} "swap_induct_false" |
1498 [Simplifier.simproc @{theory} "swap_induct_false" |
1499 ["induct_false ==> PROP P ==> PROP Q"] |
1499 ["induct_false ==> PROP P ==> PROP Q"] |