simplified Symtab;
authorwenzelm
Sun Jul 08 19:51:52 2007 +0200 (2007-07-08)
changeset 2365294eeb79be496
parent 23651 6e0b8b6012c9
child 23653 560f8f41ade2
simplified Symtab;
doc-src/IsarImplementation/Thy/ML.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Jul 08 19:51:51 2007 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Jul 08 19:51:52 2007 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4  
     1.5  text {*
     1.6    \begin{mldecls}
     1.7 -  @{index_ML_exc AList.DUP} \\
     1.8 +  @{index_ML_exn AList.DUP} \\
     1.9    @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
    1.10    @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
    1.11    @{index_ML AList.update: "('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list"} \\
    1.12 @@ -302,31 +302,27 @@
    1.13  
    1.14  text {*
    1.15    \begin{mldecls}
    1.16 -  @{index_ML_type Symtab.key} \\
    1.17    @{index_ML_type "'a Symtab.table"} \\
    1.18 -  @{index_ML_exc Symtab.DUP: Symtab.key} \\
    1.19 -  @{index_ML_exc Symtab.DUPS: "Symtab.key list"} \\
    1.20 -  @{index_ML_exc Symtab.SAME} \\
    1.21 -  @{index_ML_exc Symtab.UNDEF: Symtab.key} \\
    1.22 +  @{index_ML_exn Symtab.DUP: string} \\
    1.23 +  @{index_ML_exn Symtab.SAME} \\
    1.24 +  @{index_ML_exn Symtab.UNDEF: string} \\
    1.25    @{index_ML Symtab.empty: "'a Symtab.table"} \\
    1.26 -  @{index_ML Symtab.dest: "'a Symtab.table -> (Symtab.key * 'a) list"} \\
    1.27 -  @{index_ML Symtab.keys: "'a Symtab.table -> Symtab.key list"} \\
    1.28 -  @{index_ML Symtab.lookup: "'a Symtab.table -> Symtab.key -> 'a option"} \\
    1.29 -  @{index_ML Symtab.defined: "'a Symtab.table -> Symtab.key -> bool"} \\
    1.30 -  @{index_ML Symtab.update: "(Symtab.key * 'a) -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.31 -  @{index_ML Symtab.default: "Symtab.key * 'a -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.32 -  @{index_ML Symtab.delete: "Symtab.key
    1.33 +  @{index_ML Symtab.lookup: "'a Symtab.table -> string -> 'a option"} \\
    1.34 +  @{index_ML Symtab.defined: "'a Symtab.table -> string -> bool"} \\
    1.35 +  @{index_ML Symtab.update: "(string * 'a) -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.36 +  @{index_ML Symtab.default: "string * 'a -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.37 +  @{index_ML Symtab.delete: "string
    1.38      -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)"} \\
    1.39 -  @{index_ML Symtab.map_entry: "Symtab.key -> ('a -> 'a)
    1.40 +  @{index_ML Symtab.map_entry: "string -> ('a -> 'a)
    1.41      -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.42 -  @{index_ML Symtab.map_default: "(Symtab.key * 'a) -> ('a -> 'a)
    1.43 +  @{index_ML Symtab.map_default: "(string * 'a) -> ('a -> 'a)
    1.44      -> 'a Symtab.table -> 'a Symtab.table"} \\
    1.45 -  @{index_ML Symtab.join: "(Symtab.key -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)
    1.46 +  @{index_ML Symtab.join: "(string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)
    1.47      -> 'a Symtab.table * 'a Symtab.table
    1.48 -    -> 'a Symtab.table (*exception Symtab.DUPS*)"} \\
    1.49 +    -> 'a Symtab.table (*exception Symtab.DUP*)"} \\
    1.50    @{index_ML Symtab.merge: "('a * 'a -> bool)
    1.51      -> 'a Symtab.table * 'a Symtab.table
    1.52 -    -> 'a Symtab.table (*exception Symtab.DUPS*)"}
    1.53 +    -> 'a Symtab.table (*exception Symtab.DUP*)"}
    1.54    \end{mldecls}
    1.55  *}
    1.56  
    1.57 @@ -344,6 +340,7 @@
    1.58    Most table functions correspond to those of association lists.
    1.59  *}
    1.60  
    1.61 +
    1.62  chapter {* Cookbook *}
    1.63  
    1.64  section {* A method that depends on declarations in the context *}