--- a/src/HOL/Library/Eval.thy Tue Jan 15 16:19:21 2008 +0100
+++ b/src/HOL/Library/Eval.thy Tue Jan 15 16:19:23 2008 +0100
@@ -295,21 +295,21 @@
abbreviation (in pure_term_syntax) (input)
intT :: "typ"
where
- "intT \<equiv> Type (STR ''IntDef.int'') []"
+ "intT \<equiv> Type (STR ''Int.int'') []"
abbreviation (in pure_term_syntax) (input)
bitT :: "typ"
where
- "bitT \<equiv> Type (STR ''Numeral.bit'') []"
+ "bitT \<equiv> Type (STR ''Int.bit'') []"
function (in pure_term_syntax)
mk_int :: "int \<Rightarrow> term"
where
- "mk_int k = (if k = 0 then STR ''Numeral.Pls'' \<Colon>\<subseteq> intT
- else if k = -1 then STR ''Numeral.Min'' \<Colon>\<subseteq> intT
+ "mk_int k = (if k = 0 then STR ''Int.Pls'' \<Colon>\<subseteq> intT
+ else if k = -1 then STR ''Int.Min'' \<Colon>\<subseteq> intT
else let (l, m) = divAlg (k, 2)
- in STR ''Numeral.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
- (if m = 0 then STR ''Numeral.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Numeral.bit.B1'' \<Colon>\<subseteq> bitT))"
+ in STR ''Int.Bit'' \<Colon>\<subseteq> intT \<rightarrow> bitT \<rightarrow> intT \<bullet> mk_int l \<bullet>
+ (if m = 0 then STR ''Int.bit.B0'' \<Colon>\<subseteq> bitT else STR ''Int.bit.B1'' \<Colon>\<subseteq> bitT))"
by pat_completeness auto
termination (in pure_term_syntax)
by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
@@ -317,7 +317,7 @@
declare pure_term_syntax.mk_int.simps [code func]
definition (in pure_term_syntax)
- "term_of_int_aux k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
+ "term_of_int_aux k = STR ''Int.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
declare pure_term_syntax.term_of_int_aux_def [code func]