src/Pure/Isar/isar_syn.ML
changeset 40399 a3acca2bddc9
parent 40395 4985aaade799
child 40784 177e8cea3e09
equal deleted inserted replaced
40398:cdda2847a91e 40399:a3acca2bddc9
   500 
   500 
   501 val _ =
   501 val _ =
   502   Outer_Syntax.local_theory_to_proof "example_proof"
   502   Outer_Syntax.local_theory_to_proof "example_proof"
   503     "example proof body, without any result" Keyword.thy_schematic_goal
   503     "example proof body, without any result" Keyword.thy_schematic_goal
   504     (Scan.succeed
   504     (Scan.succeed
   505       (Specification.schematic_theorem_cmd "" NONE (K I)
   505       (Specification.theorem_cmd "" NONE (K I)
   506         Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
   506         Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
   507 
   507 
   508 val _ =
   508 val _ =
   509   Outer_Syntax.command "have" "state local goal"
   509   Outer_Syntax.command "have" "state local goal"
   510     (Keyword.tag_proof Keyword.prf_goal)
   510     (Keyword.tag_proof Keyword.prf_goal)