--- a/src/HOL/Extraction/Higman.thy Sun Aug 24 14:42:22 2008 +0200
+++ b/src/HOL/Extraction/Higman.thy Sun Aug 24 14:42:24 2008 +0200
@@ -339,6 +339,17 @@
subsection {* Some examples *}
+instantiation LT and TT :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
(* an attempt to express examples in HOL -- function
mk_word :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
where
@@ -354,16 +365,12 @@
by pat_completeness auto
termination by (relation "measure ((op -) 1001)") auto
-fun
+primrec
mk_word' :: "nat \<Rightarrow> randseed \<Rightarrow> letter list \<times> randseed"
where
"mk_word' 0 = mk_word 0"
| "mk_word' (Suc n) = (do _ \<leftarrow> mk_word 0; mk_word' n done)"*)
-consts_code
- "arbitrary :: LT" ("({* L0 [] [] *})")
- "arbitrary :: TT" ("({* T0 A [] [] [] R0 *})")
-
code_module Higman
contains
higman = higman_idx
@@ -415,17 +422,6 @@
end;
*}
-definition
- arbitrary_LT :: LT where
- [symmetric, code inline]: "arbitrary_LT = arbitrary"
-
-definition
- arbitrary_TT :: TT where
- [symmetric, code inline]: "arbitrary_TT = arbitrary"
-
-code_datatype L0 L1 arbitrary_LT
-code_datatype T0 T1 T2 arbitrary_TT
-
ML {*
val a = 16807.0;
val m = 2147483647.0;