src/Pure/pure.ML
changeset 5905 68cdba6c178f
parent 5863 9935800edf58
child 6192 a42dbf1af868
equal deleted inserted replaced
5904:e077a0e66563 5905:68cdba6c178f
    16   structure Pure =
    16   structure Pure =
    17   struct
    17   struct
    18     val thy =
    18     val thy =
    19       PureThy.begin_theory "Pure" [ProtoPure.thy]
    19       PureThy.begin_theory "Pure" [ProtoPure.thy]
    20       |> Theory.add_syntax Syntax.pure_appl_syntax
    20       |> Theory.add_syntax Syntax.pure_appl_syntax
    21       |> Theory.apply common_setup
    21       |> Library.apply common_setup
    22       |> PureThy.end_theory;
    22       |> PureThy.end_theory;
    23   end;
    23   end;
    24 
    24 
    25   structure CPure =
    25   structure CPure =
    26   struct
    26   struct
    27     val thy =
    27     val thy =
    28       PureThy.begin_theory "CPure" [ProtoPure.thy]
    28       PureThy.begin_theory "CPure" [ProtoPure.thy]
    29       |> Theory.add_syntax Syntax.pure_applC_syntax
    29       |> Theory.add_syntax Syntax.pure_applC_syntax
    30       |> Theory.apply common_setup
    30       |> Library.apply common_setup
    31       |> Theory.copy
    31       |> Theory.copy
    32       |> PureThy.end_theory;
    32       |> PureThy.end_theory;
    33   end;
    33   end;
    34 end;
    34 end;
    35 
    35