src/HOL/Typerep.thy
changeset 29574 5897b2688ccc
parent 28965 1de908189869
child 31031 cbec39ebf8f2
     1.1 --- a/src/HOL/Typerep.thy	Mon Jan 19 13:37:24 2009 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Wed Jan 21 16:47:01 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      HOL/Library/RType.thy
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Typerep.thy
     1.7      Author:     Florian Haftmann, TU Muenchen
     1.8  *)
     1.9  
    1.10 @@ -15,9 +14,7 @@
    1.11    fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
    1.12  begin
    1.13  
    1.14 -definition
    1.15 -  typerep_of :: "'a \<Rightarrow> typerep"
    1.16 -where
    1.17 +definition typerep_of :: "'a \<Rightarrow> typerep" where
    1.18    [simp]: "typerep_of x = typerep TYPE('a)"
    1.19  
    1.20  end