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+
−