equal
deleted
inserted
replaced
80 page 248: Pow has the rules |
80 page 248: Pow has the rules |
81 PowI A<=B ==> A: Pow(B) |
81 PowI A<=B ==> A: Pow(B) |
82 PowD A: Pow(B) ==> A<=B |
82 PowD A: Pow(B) ==> A<=B |
83 |
83 |
84 page 259: HOL theory files may now include datatype declarations, primitive |
84 page 259: HOL theory files may now include datatype declarations, primitive |
85 recursive function definitions, and (co)inductive definitions. (Three |
85 recursive function definitions, and (co)inductive definitions. (These new |
86 sections added.) |
86 sections are available separately as the file ml/HOL-extensions.dvi.gz, |
|
87 host ftp.cl.cam.ac.uk.) |
87 |
88 |
88 page 259: now there is another examples directory, IMP (a semantics |
89 page 259: now there is another examples directory, IMP (a semantics |
89 equivalence proof for an imperative language) |
90 equivalence proof for an imperative language) |