equal
deleted
inserted
replaced
121 (Toplevel.theory o fold add_spark_type_cmd)); |
121 (Toplevel.theory o fold add_spark_type_cmd)); |
122 |
122 |
123 val _ = |
123 val _ = |
124 Outer_Syntax.command @{command_spec "spark_vc"} |
124 Outer_Syntax.command @{command_spec "spark_vc"} |
125 "enter into proof mode for a specific verification condition" |
125 "enter into proof mode for a specific verification condition" |
126 (Parse.name >> (fn name => |
126 (Parse.name >> (fn name => Toplevel.local_theory_to_proof NONE (prove_vc name))); |
127 (Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name)))); |
|
128 |
127 |
129 val _ = |
128 val _ = |
130 Outer_Syntax.improper_command @{command_spec "spark_status"} |
129 Outer_Syntax.improper_command @{command_spec "spark_status"} |
131 "show the name and state of all loaded verification conditions" |
130 "show the name and state of all loaded verification conditions" |
132 (Scan.optional |
131 (Scan.optional |