summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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

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 52: the declaration "types bool,nat" is illegal *page 217 and 251: fst and snd should be fst_conv and snd_conv. *Also affects index: pages 310 and 317! pages 222, 223: The braces need escaping in \tdx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>} \tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>} \tdx{lfp_def} lfp(D,h) == Inter({X: Pow(D). h(X) <= X}) \tdx{gfp_def} gfp(D,h) == Union({X: Pow(D). X <= h(X)}) *page 224: type of id, namely $\To i$, should be $i \To i$ Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc] should be addsimps 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?): there is a 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