equal
deleted
inserted
replaced
240 Unsynchronized.change state_ref o Proof.goal_message o K |
240 Unsynchronized.change state_ref o Proof.goal_message o K |
241 o Pretty.chunks o cons (Pretty.str "") o single |
241 o Pretty.chunks o cons (Pretty.str "") o single |
242 o Pretty.mark Isabelle_Markup.hilite |
242 o Pretty.mark Isabelle_Markup.hilite |
243 else |
243 else |
244 print o Pretty.string_of |
244 print o Pretty.string_of |
|
245 val pprint_a = pprint Output.urgent_message |
245 fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f |
246 fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f |
246 fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f |
247 fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f |
247 fun pprint_d f = () |> debug ? pprint tracing o f |
248 fun pprint_d f = () |> debug ? pprint tracing o f |
248 val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs |
249 val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs |
249 (* |
250 (* |
668 got_all_user_axioms andalso none_true wfs andalso |
669 got_all_user_axioms andalso none_true wfs andalso |
669 sound_finitizes andalso total_consts <> SOME true andalso |
670 sound_finitizes andalso total_consts <> SOME true andalso |
670 codatatypes_ok |
671 codatatypes_ok |
671 fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) |
672 fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts) |
672 in |
673 in |
673 (pprint_n (fn () => Pretty.chunks |
674 (pprint_a (Pretty.chunks |
674 [Pretty.blk (0, |
675 [Pretty.blk (0, |
675 (pstrs ((if mode = Auto_Try then "Auto " else "") ^ |
676 (pstrs ((if mode = Auto_Try then "Auto " else "") ^ |
676 "Nitpick found a" ^ |
677 "Nitpick found a" ^ |
677 (if not genuine then " potentially spurious " |
678 (if not genuine then " potentially spurious " |
678 else if genuine_means_genuine then " " |
679 else if genuine_means_genuine then " " |