doc-src/ERRATA.txt
author lcp
Wed, 27 Jul 1994 19:04:21 +0200
changeset 491 1a7717eca145
parent 479 db5a95f2952e
child 507 a00301e9e64b
permissions -rw-r--r--
logics update
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
456
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     1
ERRATA in Springer book
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     2
491
1a7717eca145 logics update
lcp
parents: 479
diff changeset
     3
Thanks to Sara Kalvala, Tobias Nipkow
1a7717eca145 logics update
lcp
parents: 479
diff changeset
     4
456
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     5
* = corrected by sending new pages
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     6
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     7
*page 50: In section heading, Mixfix should be mixfix
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     8
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
     9
page 52: the declaration  "types bool,nat"  is illegal    
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    10
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    11
*page 217 and 251: fst and snd should be fst_conv and snd_conv.
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    12
*Also affects index: pages 310 and 317!
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    13
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    14
pages 222, 223: The braces need escaping in
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    15
\tdx{qconverse_def}   qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    16
\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {<x;y>}
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    17
\tdx{lfp_def}        lfp(D,h) == Inter({X: Pow(D). h(X) <= X})
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    18
\tdx{gfp_def}        gfp(D,h) == Union({X: Pow(D). X <= h(X)})
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    19
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    20
*page 224: type of id, namely $\To i$, should be $i \To i$ 
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    21
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    22
Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc]
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    23
should be addsimps
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    24
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    25
Ref/tactic: documented subgoals_tac
f1df7fc211a7 New errata list for the documentation
lcp
parents:
diff changeset
    26
491
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    27
Ref/theories: added init_thy_reader and removed extend_theory.
458
877704b91847 type constraints
nipkow
parents: 456
diff changeset
    28
877704b91847 type constraints
nipkow
parents: 456
diff changeset
    29
Ref/defining: type constraints ("::") now have a very low priority of 4.
877704b91847 type constraints
nipkow
parents: 456
diff changeset
    30
              As in ML, they must be enclosed in paretheses most of the time.
479
db5a95f2952e *** empty log message ***
nipkow
parents: 458
diff changeset
    31
491
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    32
Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file"
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    33
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    34
Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    35
renamed union_iff to Union_iff
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    36
renamed power_set to Pow_iff
1a7717eca145 logics update
lcp
parents: 479
diff changeset
    37
DiffD2: now is really a destruction rule