updated;
authorwenzelm
Sun Jul 08 19:51:54 2007 +0200 (2007-07-08)
changeset 23653560f8f41ade2
parent 23652 94eeb79be496
child 23654 a2ad1c166ac8
updated;
doc-src/IsarImplementation/Thy/document/ML.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Jul 08 19:51:52 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sun Jul 08 19:51:54 2007 +0200
     1.3 @@ -430,31 +430,27 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  \begin{mldecls}
     1.7 -  \indexmltype{Symtab.key}\verb|type Symtab.key| \\
     1.8    \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
     1.9 -  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of Symtab.key| \\
    1.10 -  \indexmlexception{Symtab.DUPS}\verb|exception Symtab.DUPS of Symtab.key list| \\
    1.11 +  \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
    1.12    \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
    1.13 -  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of Symtab.key| \\
    1.14 +  \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
    1.15    \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
    1.16 -  \indexml{Symtab.dest}\verb|Symtab.dest: 'a Symtab.table -> (Symtab.key * 'a) list| \\
    1.17 -  \indexml{Symtab.keys}\verb|Symtab.keys: 'a Symtab.table -> Symtab.key list| \\
    1.18 -  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> Symtab.key -> 'a option| \\
    1.19 -  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> Symtab.key -> bool| \\
    1.20 -  \indexml{Symtab.update}\verb|Symtab.update: (Symtab.key * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
    1.21 -  \indexml{Symtab.default}\verb|Symtab.default: Symtab.key * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
    1.22 -  \indexml{Symtab.delete}\verb|Symtab.delete: Symtab.key|\isasep\isanewline%
    1.23 +  \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
    1.24 +  \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
    1.25 +  \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
    1.26 +  \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
    1.27 +  \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
    1.28  \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
    1.29 -  \indexml{Symtab.map-entry}\verb|Symtab.map_entry: Symtab.key -> ('a -> 'a)|\isasep\isanewline%
    1.30 +  \indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
    1.31  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
    1.32 -  \indexml{Symtab.map-default}\verb|Symtab.map_default: (Symtab.key * 'a) -> ('a -> 'a)|\isasep\isanewline%
    1.33 +  \indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
    1.34  \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
    1.35 -  \indexml{Symtab.join}\verb|Symtab.join: (Symtab.key -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
    1.36 +  \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
    1.37  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
    1.38 -\verb|    -> 'a Symtab.table (*exception Symtab.DUPS*)| \\
    1.39 +\verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
    1.40    \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
    1.41  \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
    1.42 -\verb|    -> 'a Symtab.table (*exception Symtab.DUPS*)|
    1.43 +\verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
    1.44    \end{mldecls}%
    1.45  \end{isamarkuptext}%
    1.46  \isamarkuptrue%