doc-src/IsarImplementation/Thy/document/ML.tex
changeset 23653 560f8f41ade2
parent 22550 c5039bee2602
child 24089 070d539ba403
equal deleted inserted replaced
23652:94eeb79be496 23653:560f8f41ade2
   428 }
   428 }
   429 \isamarkuptrue%
   429 \isamarkuptrue%
   430 %
   430 %
   431 \begin{isamarkuptext}%
   431 \begin{isamarkuptext}%
   432 \begin{mldecls}
   432 \begin{mldecls}
   433   \indexmltype{Symtab.key}\verb|type Symtab.key| \\
       
   434   \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
   433   \indexmltype{'a Symtab.table}\verb|type 'a Symtab.table| \\
   435   \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of Symtab.key| \\
   434   \indexmlexception{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
   436   \indexmlexception{Symtab.DUPS}\verb|exception Symtab.DUPS of Symtab.key list| \\
       
   437   \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
   435   \indexmlexception{Symtab.SAME}\verb|exception Symtab.SAME| \\
   438   \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of Symtab.key| \\
   436   \indexmlexception{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
   439   \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   437   \indexml{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
   440   \indexml{Symtab.dest}\verb|Symtab.dest: 'a Symtab.table -> (Symtab.key * 'a) list| \\
   438   \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
   441   \indexml{Symtab.keys}\verb|Symtab.keys: 'a Symtab.table -> Symtab.key list| \\
   439   \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
   442   \indexml{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> Symtab.key -> 'a option| \\
   440   \indexml{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   443   \indexml{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> Symtab.key -> bool| \\
   441   \indexml{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
   444   \indexml{Symtab.update}\verb|Symtab.update: (Symtab.key * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
   442   \indexml{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
   445   \indexml{Symtab.default}\verb|Symtab.default: Symtab.key * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
       
   446   \indexml{Symtab.delete}\verb|Symtab.delete: Symtab.key|\isasep\isanewline%
       
   447 \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
   443 \verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
   448   \indexml{Symtab.map-entry}\verb|Symtab.map_entry: Symtab.key -> ('a -> 'a)|\isasep\isanewline%
   444   \indexml{Symtab.map-entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
   449 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   445 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   450   \indexml{Symtab.map-default}\verb|Symtab.map_default: (Symtab.key * 'a) -> ('a -> 'a)|\isasep\isanewline%
   446   \indexml{Symtab.map-default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
   451 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   447 \verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
   452   \indexml{Symtab.join}\verb|Symtab.join: (Symtab.key -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   448   \indexml{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
   453 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   449 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   454 \verb|    -> 'a Symtab.table (*exception Symtab.DUPS*)| \\
   450 \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
   455   \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   451   \indexml{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
   456 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   452 \verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
   457 \verb|    -> 'a Symtab.table (*exception Symtab.DUPS*)|
   453 \verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
   458   \end{mldecls}%
   454   \end{mldecls}%
   459 \end{isamarkuptext}%
   455 \end{isamarkuptext}%
   460 \isamarkuptrue%
   456 \isamarkuptrue%
   461 %
   457 %
   462 \begin{isamarkuptext}%
   458 \begin{isamarkuptext}%