# HG changeset patch
# User haftmann
# Date 1179567204 -7200
# Node ID abecb6a8cea6873bc4a9d3f4099d26b3b1fb76dd
# Parent  019d44d4683483fd00a51478c8cc44e7d4058b5f
typ_of instance for int

diff -r 019d44d46834 -r abecb6a8cea6 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Sat May 19 11:33:23 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Sat May 19 11:33:24 2007 +0200
@@ -34,6 +34,9 @@
 end;
 *}
 
+instance int :: typ_of
+  "typ_of T \<equiv> STR ''IntDef.int'' {\<struct>} []" ..
+
 setup {*
 let
   fun mk arities _ thy =