# HG changeset patch
# User haftmann
# Date 1232552821 -3600
# Node ID 5897b2688cccb343ea4446fcc21a85b6979eab87
# Parent  fa6c5d62adf59d2fb9d79147f84975f1256eaf1f
tuned

diff -r fa6c5d62adf5 -r 5897b2688ccc src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Mon Jan 19 13:37:24 2009 +0100
+++ b/src/HOL/Typerep.thy	Wed Jan 21 16:47:01 2009 +0100
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Library/RType.thy
-    ID:         $Id$
+(*  Title:      HOL/Typerep.thy
     Author:     Florian Haftmann, TU Muenchen
 *)
 
@@ -15,9 +14,7 @@
   fixes typerep :: "'a\<Colon>{} itself \<Rightarrow> typerep"
 begin
 
-definition
-  typerep_of :: "'a \<Rightarrow> typerep"
-where
+definition typerep_of :: "'a \<Rightarrow> typerep" where
   [simp]: "typerep_of x = typerep TYPE('a)"
 
 end