1 theory Command

     2 imports Main

     3 begin

     4 ML {*

     5 let

     6    val do_nothing = Scan.succeed (LocalTheory.theory I)

     7    val kind = OuterKeyword.thy_goal

     8 in

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

    10 end

    11 *}

    12 

    13 ML {*

    14 let

    15    val do_nothing = Scan.succeed (LocalTheory.theory I)

    16    val kind = OuterKeyword.thy_decl

    17 in

    18    OuterSyntax.local_theory "simple_induct" "description of foobar" kind do_nothing

    19 end

    20 *}

    21 

    22 end