src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 18358 0a733e11021a
parent 17925 80a528111a82
child 18443 a1d53af4c4c7
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Dec 06 06:22:14 2005 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Dec 06 09:04:09 2005 +0100
     1.3 @@ -1,19 +1,19 @@
     1.4  (*  Title:      HOLCF/IOA/meta_theory/ioa_package.ML
     1.5      ID:         $Id$
     1.6 -    Author:	Tobias Hamberger, TU Muenchen
     1.7 +    Author:     Tobias Hamberger, TU Muenchen
     1.8  *)
     1.9  
    1.10  signature IOA_PACKAGE =
    1.11  sig
    1.12 - val add_ioa: string -> string ->
    1.13 -		 (string) list -> (string) list -> (string) list ->
    1.14 -		(string * string) list -> string ->
    1.15 -		(string * string * (string * string)list) list
    1.16 -	-> theory -> theory
    1.17 - val add_composition : string -> (string)list -> theory -> theory
    1.18 - val add_hiding : string -> string -> (string)list -> theory -> theory
    1.19 - val add_restriction : string -> string -> (string)list -> theory -> theory
    1.20 - val add_rename : string -> string -> string -> theory -> theory
    1.21 +  val add_ioa: string -> string
    1.22 +    -> (string) list -> (string) list -> (string) list
    1.23 +    -> (string * string) list -> string
    1.24 +    -> (string * string * (string * string)list) list
    1.25 +    -> theory -> theory
    1.26 +  val add_composition : string -> (string)list -> theory -> theory
    1.27 +  val add_hiding : string -> string -> (string)list -> theory -> theory
    1.28 +  val add_restriction : string -> string -> (string)list -> theory -> theory
    1.29 +  val add_rename : string -> string -> string -> theory -> theory
    1.30  end;
    1.31  
    1.32  structure IoaPackage: IOA_PACKAGE =
    1.33 @@ -353,7 +353,7 @@
    1.34  (automaton_name ^ "_trans",
    1.35   "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
    1.36  (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
    1.37 -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
    1.38 +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    1.39  [(automaton_name ^ "_initial_def",
    1.40  automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
    1.41  (automaton_name ^ "_asig_def",
    1.42 @@ -394,7 +394,7 @@
    1.43    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    1.44     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    1.45  ,NoSyn)]
    1.46 -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
    1.47 +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    1.48  [(automaton_name ^ "_def",
    1.49  automaton_name ^ " == " ^ comp_list)]
    1.50  end)
    1.51 @@ -409,7 +409,7 @@
    1.52  thy
    1.53  |> ContConsts.add_consts_i
    1.54  [(automaton_name, auttyp,NoSyn)]
    1.55 -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
    1.56 +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    1.57  [(automaton_name ^ "_def",
    1.58  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
    1.59  end)
    1.60 @@ -423,7 +423,7 @@
    1.61  thy
    1.62  |> ContConsts.add_consts_i
    1.63  [(automaton_name, auttyp,NoSyn)]
    1.64 -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
    1.65 +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    1.66  [(automaton_name ^ "_def",
    1.67  automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
    1.68  end)
    1.69 @@ -449,7 +449,7 @@
    1.70    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    1.71     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    1.72  ,NoSyn)]
    1.73 -|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
    1.74 +|> (snd oo (PureThy.add_defs false o map Thm.no_attributes))
    1.75  [(automaton_name ^ "_def",
    1.76  automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
    1.77  end)