doc-src/ERRATA.txt
author lcp
Thu Aug 04 11:45:59 1994 +0200 (1994-08-04)
changeset 507 a00301e9e64b
parent 491 1a7717eca145
child 599 08b403fe92b1
permissions -rw-r--r--
addition of show_brackets
lcp@456
     1
ERRATA in Springer book
lcp@456
     2
lcp@491
     3
Thanks to Sara Kalvala, Tobias Nipkow
lcp@491
     4
lcp@456
     5
* = corrected by sending new pages
lcp@456
     6
lcp@456
     7
*page 50: In section heading, Mixfix should be mixfix
lcp@456
     8
lcp@456
     9
*page 217 and 251: fst and snd should be fst_conv and snd_conv.
lcp@456
    10
*Also affects index: pages 310 and 317!
lcp@456
    11
lcp@456
    12
*page 224: type of id, namely $\To i$, should be $i \To i$ 
lcp@456
    13
lcp@507
    14
Intro/advanced
lcp@507
    15
page 52: the declaration  "types bool,nat"  is illegal    
lcp@507
    16
lcp@507
    17
should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
lcp@507
    18
lcp@507
    19
lcp@507
    20
Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
lcp@507
    21
lcp@507
    22
Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
lcp@456
    23
lcp@456
    24
Ref/tactic: documented subgoals_tac
lcp@456
    25
lcp@491
    26
Ref/theories: added init_thy_reader and removed extend_theory.
nipkow@458
    27
nipkow@458
    28
Ref/defining: type constraints ("::") now have a very low priority of 4.
nipkow@458
    29
              As in ML, they must be enclosed in paretheses most of the time.
nipkow@479
    30
lcp@507
    31
Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
lcp@491
    32
lcp@507
    33
Logics/ZF: ****************
lcp@507
    34
renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
lcp@491
    35
renamed union_iff to Union_iff
lcp@491
    36
renamed power_set to Pow_iff
lcp@491
    37
DiffD2: now is really a destruction rule
lcp@507
    38
escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
lcp@507
    39