theory Command

imports Main

begin

ML {*

let

   val do_nothing = Scan.succeed (Local_Theory.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 =

     Local_Theory.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 =

        Local_Theory.note (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 (Local_Theory.theory I)

   val kind = OuterKeyword.thy_decl

in

   OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing

end

*}*)

end