theory Command
imports Main
begin

ML {*
let
   val do_nothing = Scan.succeed (LocalTheory.theory I)
   val kind = OuterKeyword.thy_decl
in
   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
end
*}

ML {*
let
  fun trace_prop str =
     LocalTheory.theory (fn lthy => (tracing str; lthy))
  val trace_prop_parser = OuterParse.prop >> trace_prop
  val kind = OuterKeyword.thy_decl
in
  OuterSyntax.local_theory "foobar_trace" "traces a proposition"
    kind trace_prop_parser
end
*}

ML {*
let
   fun prove_prop str lthy =
     let
       val prop = Syntax.read_prop lthy str
     in
       Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
     end;
   val prove_prop_parser = OuterParse.prop >> prove_prop
   val kind = OuterKeyword.thy_goal
in
   OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition"
     kind prove_prop_parser
end
*}

ML {*
val r = Unsynchronized.ref (NONE:(unit -> term) option)
*}
ML{*
let
   fun after_qed thm_name thms lthy =
        LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd

   fun setup_proof (thm_name, (txt, pos)) lthy =
   let
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
     Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy
   end

   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
 
in
   OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
     OuterKeyword.thy_goal (parser >> setup_proof)
end*}


(*
ML {*
let
   val do_nothing = Scan.succeed (LocalTheory.theory I)
   val kind = OuterKeyword.thy_decl
in
   OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing
end
*}*)

end