src/Pure/Isar/proof.ML
changeset 51048 123be08eed88
parent 50912 8d391f185cac
child 51222 8c3e5fb41139
equal deleted inserted replaced
51047:2ad5c46bcd04 51048:123be08eed88
  1029 (* skip proofs *)
  1029 (* skip proofs *)
  1030 
  1030 
  1031 local
  1031 local
  1032 
  1032 
  1033 fun skipped_proof state =
  1033 fun skipped_proof state =
  1034   Context_Position.report_text (context_of state) (Position.thread_data ())
  1034   Context_Position.if_visible (context_of state) Output.report
  1035     Markup.bad "Skipped proof";
  1035     (Markup.markup Markup.bad "Skipped proof");
  1036 
  1036 
  1037 in
  1037 in
  1038 
  1038 
  1039 fun local_skip_proof int state =
  1039 fun local_skip_proof int state =
  1040   local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
  1040   local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before