diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Helper/Command/Command.thy --- a/ProgTutorial/Helper/Command/Command.thy Tue May 14 16:59:53 2019 +0200 +++ b/ProgTutorial/Helper/Command/Command.thy Tue May 14 17:10:47 2019 +0200 @@ -4,7 +4,7 @@ "foobar_goal" "foobar_prove" :: thy_goal begin -ML {* +ML \<open> let val do_nothing = Scan.succeed (Local_Theory.background_theory I) in @@ -12,9 +12,9 @@ "description of foobar" do_nothing end -*} +\<close> -ML {* +ML \<open> let fun trace_prop str = Local_Theory.background_theory (fn lthy => (tracing str; lthy)) @@ -24,9 +24,9 @@ "traces a proposition" trace_prop_parser end -*} +\<close> -ML {* +ML \<open> let fun prove_prop str lthy = let @@ -40,17 +40,17 @@ "proving a proposition" prove_prop_parser end -*} +\<close> -ML {* +ML \<open> structure Result = Proof_Data( type T = unit -> term fun init thy () = error "Result") val result_cookie = (Result.get, Result.put, "Result.put") -*} +\<close> -ML{* +ML\<open> let fun after_qed thm_name thms lthy = Local_Theory.note (thm_name, (flat thms)) lthy |> snd @@ -68,7 +68,7 @@ Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} "proving a proposition" (parser >> setup_proof) -end*} +end\<close>