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

author | blanchet |

Fri, 11 May 2012 01:02:36 +0200 | |

changeset 47910 | ca5b629a5995 |

parent 47909 | 5f1afeebafbc |

child 47911 | 2168126446bb |

reintroduced example now that it's no longer broken

--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri May 11 00:45:24 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri May 11 01:02:36 2012 +0200 @@ -176,9 +176,7 @@ by (fact Rep_point_ext_inverse) lemma "Fract a b = of_int a / of_int b" -(* FIXME: broken by conversion of Rat.thy to lift_definition/transfer. nitpick [card = 1, expect = none] -*) by (rule Fract_of_int_quotient) lemma "Abs_rat (Rep_rat a) = a"