doc-src/ERRATA.txt
author lcp
Wed, 17 Aug 1994 10:42:41 +0200
changeset 541 be4c4ba87143
parent 507 a00301e9e64b
child 599 08b403fe92b1
permissions -rw-r--r--
overheads for inductive definitions, originally for CADE-12

ERRATA in Springer book

Thanks to Sara Kalvala, Tobias Nipkow

* = corrected by sending new pages

*page 50: In section heading, Mixfix should be mixfix

*page 217 and 251: fst and snd should be fst_conv and snd_conv.
*Also affects index: pages 310 and 317!

*page 224: type of id, namely $\To i$, should be $i \To i$ 

Intro/advanced
page 52: the declaration  "types bool,nat"  is illegal    

should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'


Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}

Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}

Ref/tactic: documented subgoals_tac

Ref/theories: added init_thy_reader and removed extend_theory.

Ref/defining: type constraints ("::") now have a very low priority of 4.
              As in ML, they must be enclosed in paretheses most of the time.

Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"

Logics/ZF: ****************
renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
renamed union_iff to Union_iff
renamed power_set to Pow_iff
DiffD2: now is really a destruction rule
escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def