equal
deleted
inserted
replaced
1024 end; |
1024 end; |
1025 |
1025 |
1026 |
1026 |
1027 (* skip proofs *) |
1027 (* skip proofs *) |
1028 |
1028 |
1029 local |
|
1030 |
|
1031 fun skipped_proof state = |
|
1032 Context_Position.if_visible (context_of state) Output.report |
|
1033 (Markup.markup Markup.bad "Skipped proof"); |
|
1034 |
|
1035 in |
|
1036 |
|
1037 fun local_skip_proof int state = |
1029 fun local_skip_proof int state = |
1038 local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |
1030 local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |
1039 skipped_proof state; |
1031 Skip_Proof.report (context_of state); |
1040 |
1032 |
1041 fun global_skip_proof int state = |
1033 fun global_skip_proof int state = |
1042 global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |
1034 global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before |
1043 skipped_proof state; |
1035 Skip_Proof.report (context_of state); |
1044 |
|
1045 end; |
|
1046 |
1036 |
1047 |
1037 |
1048 (* common goal statements *) |
1038 (* common goal statements *) |
1049 |
1039 |
1050 local |
1040 local |