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

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

end