src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 24867 e5b55d7be9bb
parent 24707 dfeb98f84e93
child 26336 a0e2b706ce73
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -481,10 +481,15 @@
     1.4    add_rename aut source_aut rename_f;
     1.5  
     1.6  
     1.7 -(* parsers *)
     1.8 +(* outer syntax *)
     1.9  
    1.10  local structure P = OuterParse and K = OuterKeyword in
    1.11  
    1.12 +val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
    1.13 +  "outputs", "internals", "states", "initially", "transitions", "pre",
    1.14 +  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
    1.15 +  "rename"];
    1.16 +
    1.17  val actionlist = P.list1 P.term;
    1.18  val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
    1.19  val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
    1.20 @@ -520,21 +525,10 @@
    1.21    (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
    1.22      >> mk_rename_decl;
    1.23  
    1.24 -val automatonP =
    1.25 +val _ =
    1.26    OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
    1.27      (ioa_decl >> Toplevel.theory);
    1.28  
    1.29  end;
    1.30  
    1.31 -
    1.32 -(* setup outer syntax *)
    1.33 -
    1.34 -val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs",
    1.35 -  "outputs", "internals", "states", "initially", "transitions", "pre",
    1.36 -  "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
    1.37 -  "rename"];
    1.38 -
    1.39 -val _ = OuterSyntax.add_parsers [automatonP];
    1.40 -
    1.41 -
    1.42  end;