equal
deleted
inserted
replaced
79 |
79 |
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 and |
84 page 259: HOL theory files may now include datatype declarations, primitive |
85 (co)inductive definitions. (Two sections added.) |
85 recursive function definitions, and (co)inductive definitions. (Three |
|
86 sections added.) |
86 |
87 |
87 page 259: now there is another examples directory, IMP (a semantics |
88 page 259: now there is another examples directory, IMP (a semantics |
88 equivalence proof for an imperative language) |
89 equivalence proof for an imperative language) |