token translation: real;
authorwenzelm
Tue Mar 09 12:06:09 1999 +0100 (1999-03-09)
changeset 631115652e058e28
parent 6310 353a8a9d9d2c
child 6312 d361b0a99e31
token translation: real;
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/sign.ML	Tue Mar 09 12:05:07 1999 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 09 12:06:09 1999 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    val add_trfunsT:
     1.5      (string * (bool -> typ -> term list -> term)) list -> sg -> sg
     1.6    val add_tokentrfuns:
     1.7 -    (string * string * (string -> string * int)) list -> sg -> sg
     1.8 +    (string * string * (string -> string * real)) list -> sg -> sg
     1.9    val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
    1.10    val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    1.11    val add_path: string -> sg -> sg
     2.1 --- a/src/Pure/theory.ML	Tue Mar 09 12:05:07 1999 +0100
     2.2 +++ b/src/Pure/theory.ML	Tue Mar 09 12:06:09 1999 +0100
     2.3 @@ -24,8 +24,8 @@
     2.4    val subthy: theory * theory -> bool
     2.5    val eq_thy: theory * theory -> bool
     2.6    val cert_axm: Sign.sg -> string * term -> string * term
     2.7 -  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> string list ->
     2.8 -    string * string -> string * term
     2.9 +  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    2.10 +    string list -> string * string -> string * term
    2.11    val read_axm: Sign.sg -> string * string -> string * term
    2.12    val inferT_axm: Sign.sg -> string * term -> string * term
    2.13    val merge_theories: string -> theory * theory -> theory
    2.14 @@ -65,7 +65,9 @@
    2.15    val add_trfunsT:
    2.16      (string * (bool -> typ -> term list -> term)) list -> theory -> theory
    2.17    val add_tokentrfuns:
    2.18 -    (string * string * (string -> string * int)) list -> theory -> theory
    2.19 +    (string * string * (string -> string * real)) list -> theory -> theory
    2.20 +  val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    2.21 +    -> theory -> theory
    2.22    val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    2.23    val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
    2.24    val add_axioms: (bstring * string) list -> theory -> theory
    2.25 @@ -196,6 +198,7 @@
    2.26  val add_trfuns       = ext_sign Sign.add_trfuns;
    2.27  val add_trfunsT      = ext_sign Sign.add_trfunsT;
    2.28  val add_tokentrfuns  = ext_sign Sign.add_tokentrfuns;
    2.29 +fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
    2.30  val add_trrules      = ext_sign Sign.add_trrules;
    2.31  val add_trrules_i    = ext_sign Sign.add_trrules_i;
    2.32  val add_path         = ext_sign Sign.add_path;
    2.33 @@ -207,6 +210,7 @@
    2.34  val copy             = prep_ext;	(*an approximation ...*)
    2.35  
    2.36  
    2.37 +
    2.38  (** add axioms **)
    2.39  
    2.40  (* prepare axioms *)