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