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

author | haftmann |

Wed, 28 Nov 2007 15:09:19 +0100 | |

changeset 25488 | c945521fa0d9 |

parent 25487 | d96d5808d926 |

child 25489 | 5b0625f6e324 |

deleted looping code theorem

--- a/src/HOL/Library/Efficient_Nat.thy Wed Nov 28 14:56:38 2007 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Nov 28 15:09:19 2007 +0100 @@ -33,7 +33,7 @@ definition int_of_nat :: "nat \<Rightarrow> int" where - "int_of_nat n = of_nat n" + [code func del]: "int_of_nat n = of_nat n" lemma int_of_nat_Suc [simp]: "int_of_nat (Suc n) = 1 + int_of_nat n"