# HG changeset patch
# User bulwahn
# Date 1310978061 -7200
# Node ID 90d24cafb05d84ed0e621865a8bf9c918ee8758e
# Parent  ee4be704c2a476239c85ed4a32bdd454a747046f
adding code equations for partial_term_of for rational numbers

diff -r ee4be704c2a4 -r 90d24cafb05d src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
+++ b/src/HOL/Rat.thy	Mon Jul 18 10:34:21 2011 +0200
@@ -1171,6 +1171,21 @@
 
 end
 
+instantiation rat :: partial_term_of
+begin
+
+instance ..
+
+end
+
+lemma [code]:
+  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
+  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
+     Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'')
+     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [],
+        Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)" 
+by (rule partial_term_of_anything)+
+
 instantiation rat :: narrowing
 begin