src/Pure/Isar/isar.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6193 451d3d6c088f
child 6644 123b215882ae
permissions -rw-r--r--
common qed and end of proofs;
     1 (*  Title:      Pure/Isar/isar.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isabelle/Isar main interface.
     6 *)
     7 
     8 signature ISAR =
     9 sig
    10   type parser
    11   val main: unit -> unit
    12   val loop: unit -> unit
    13   val help: unit -> unit
    14   val commands: unit -> string list
    15   val add_keywords: string list -> unit
    16   val add_parsers: parser list -> unit
    17 end;
    18 
    19 structure Isar: ISAR =
    20 struct
    21 
    22 type parser = OuterSyntax.parser;
    23 val main = OuterSyntax.main;
    24 val loop = OuterSyntax.loop;
    25 val help = OuterSyntax.help;
    26 val commands = OuterSyntax.commands;
    27 val add_keywords = OuterSyntax.add_keywords;
    28 val add_parsers = OuterSyntax.add_parsers;
    29 
    30 end;