src/Pure/Isar/isar_syn.ML
changeset 7002 01a4e15ee253
parent 6972 3ae2eeabde80
child 7012 ae9dac5af9d1
equal deleted inserted replaced
7001:8121e11ed765 7002:01a4e15ee253
   341 
   341 
   342 (* end proof *)
   342 (* end proof *)
   343 
   343 
   344 val qedP =
   344 val qedP =
   345   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   345   OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
   346     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
   346     (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed);
   347 
   347 
   348 val terminal_proofP =
   348 val terminal_proofP =
   349   OuterSyntax.command "by" "terminal backward proof" K.qed
   349   OuterSyntax.command "by" "terminal backward proof" K.qed
   350     (P.method -- P.interest -- Scan.option (P.method -- P.interest) >> IsarThy.terminal_proof);
   350     (P.method -- P.interest -- Scan.option (P.method -- P.interest)
       
   351       -- P.marg_comment >> IsarThy.terminal_proof);
   351 
   352 
   352 val immediate_proofP =
   353 val immediate_proofP =
   353   OuterSyntax.command "." "immediate proof" K.qed
   354   OuterSyntax.command "." "immediate proof" K.qed
   354     (Scan.succeed IsarThy.immediate_proof);
   355     (P.marg_comment >> IsarThy.immediate_proof);
   355 
   356 
   356 val default_proofP =
   357 val default_proofP =
   357   OuterSyntax.command ".." "default proof" K.qed
   358   OuterSyntax.command ".." "default proof" K.qed
   358     (Scan.succeed IsarThy.default_proof);
   359     (P.marg_comment >> IsarThy.default_proof);
   359 
   360 
   360 val skip_proofP =
   361 val skip_proofP =
   361   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
   362   OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
   362     (Scan.succeed IsarThy.skip_proof);
   363     (P.marg_comment >> IsarThy.skip_proof);
   363 
   364 
   364 
   365 
   365 (* proof steps *)
   366 (* proof steps *)
   366 
   367 
   367 val applyP =
   368 val applyP =
   372   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   373   OuterSyntax.improper_command "then_apply" "unstructured backward proof step, using facts"
   373     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   374     K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   374 
   375 
   375 val proofP =
   376 val proofP =
   376   OuterSyntax.command "proof" "backward proof" K.prf_block
   377   OuterSyntax.command "proof" "backward proof" K.prf_block
   377     (P.interest -- Scan.option (P.method -- P.interest)
   378     (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment
   378       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   379       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   379 
   380 
   380 
   381 
   381 (* calculational proof commands *)
   382 (* calculational proof commands *)
   382 
   383