summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Mon, 23 Oct 2000 10:16:52 +0200 | |

changeset 10287 | 9ab1671398a6 |

parent 10286 | fdcdb8a80988 |

child 10288 | 00abecbfa46a |

two spelling fixes

--- a/doc-src/TutorialI/Inductive/AB.thy Sun Oct 22 22:23:16 2000 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Mon Oct 23 10:16:52 2000 +0200 @@ -18,14 +18,14 @@ At the end we say a few words about the relationship of the formalization and the text in the book~\cite[p.\ 81]{HopcroftUllman}. -We start by fixing the alpgabet, which consists only of @{term a}'s +We start by fixing the alphabet, which consists only of @{term a}'s and @{term b}'s: *} datatype alfa = a | b; text{*\noindent -For convenience we includ the following easy lemmas as simplification rules: +For convenience we include the following easy lemmas as simplification rules: *} lemma [simp]: "(x \<noteq> a) = (x = b) \<and> (x \<noteq> b) = (x = a)";