changeset 47937 | 70375fa2679d |
parent 47780 | 3357688660ff |
child 49812 | e3945ddcb9aa |
--- a/src/HOL/Library/Float.thy Wed May 16 19:15:45 2012 +0200 +++ b/src/HOL/Library/Float.thy Wed May 16 19:17:20 2012 +0200 @@ -19,7 +19,7 @@ lemma type_definition_float': "type_definition real float_of float" using type_definition_float unfolding real_of_float_def . -setup_lifting (no_abs_code) type_definition_float' +setup_lifting (no_code) type_definition_float' lemmas float_of_inject[simp]