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

author | haftmann |

Tue, 30 Sep 2008 12:49:17 +0200 | |

changeset 28422 | bfa368164502 |

parent 28421 | 05d202350b8d |

child 28423 | 9fc3befd8191 |

tuned

--- a/src/HOL/ex/NormalForm.thy Tue Sep 30 12:49:16 2008 +0200 +++ b/src/HOL/ex/NormalForm.thy Tue Sep 30 12:49:17 2008 +0200 @@ -71,7 +71,8 @@ lemma "[] @ xs = xs" by normalization lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization -lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+ +lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" + by normalization rule+ lemma "rev [a, b, c] = [c, b, a]" by normalization normal_form "rev (a#b#cs) = rev cs @ [b, a]" normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])" @@ -95,9 +96,6 @@ lemma "last [a, b, c] = c" by normalization lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization -lemma [code nbe]: - "eq_class.eq (x :: int) x \<longleftrightarrow> True" unfolding eq by rule+ - lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization lemma "(-4::int) * 2 = -8" by normalization lemma "abs ((-4::int) + 2 * 1) = 2" by normalization