equal
deleted
inserted
replaced
468 exists is_struct_induct_step (Proof_Context.cases_of ctxt) |
468 exists is_struct_induct_step (Proof_Context.cases_of ctxt) |
469 val _ = if standard andalso likely_in_struct_induct_step then |
469 val _ = if standard andalso likely_in_struct_induct_step then |
470 pprint_nt (fn () => Pretty.blk (0, |
470 pprint_nt (fn () => Pretty.blk (0, |
471 pstrs "Hint: To check that the induction hypothesis is \ |
471 pstrs "Hint: To check that the induction hypothesis is \ |
472 \general enough, try this command: " @ |
472 \general enough, try this command: " @ |
473 [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0, |
473 [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0, |
474 pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) |
474 pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) |
475 else |
475 else |
476 () |
476 () |
477 (* |
477 (* |
478 val _ = print_g "Monotonic types:" |
478 val _ = print_g "Monotonic types:" |