--- a/src/HOL/Code_Eval.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Code_Eval.thy Tue Jul 14 16:27:32 2009 +0200
@@ -32,7 +32,7 @@
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
-lemma valapp_code [code, code_inline]:
+lemma valapp_code [code, code_unfold]:
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
by (simp only: valapp_def fst_conv snd_conv)
--- a/src/HOL/Code_Numeral.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Code_Numeral.thy Tue Jul 14 16:27:32 2009 +0200
@@ -176,13 +176,13 @@
end
-lemma zero_code_numeral_code [code_inline, code]:
+lemma zero_code_numeral_code [code, code_unfold]:
"(0\<Colon>code_numeral) = Numeral0"
by (simp add: number_of_code_numeral_def Pls_def)
lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
using zero_code_numeral_code ..
-lemma one_code_numeral_code [code_inline, code]:
+lemma one_code_numeral_code [code, code_unfold]:
"(1\<Colon>code_numeral) = Numeral1"
by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Jul 14 16:27:32 2009 +0200
@@ -283,7 +283,7 @@
where
[code del]: "raise_exc e = raise []"
-lemma raise_raise_exc [code, code_inline]:
+lemma raise_raise_exc [code, code_unfold]:
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
--- a/src/HOL/Int.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Int.thy Tue Jul 14 16:27:32 2009 +0200
@@ -2126,11 +2126,11 @@
hide (open) const nat_aux
-lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
+lemma zero_is_num_zero [code, code_unfold_post]:
"(0\<Colon>int) = Numeral0"
by simp
-lemma one_is_num_one [code, code_inline, symmetric, code_post]:
+lemma one_is_num_one [code, code_unfold_post]:
"(1\<Colon>int) = Numeral1"
by simp
--- a/src/HOL/IntDiv.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/IntDiv.thy Tue Jul 14 16:27:32 2009 +0200
@@ -36,7 +36,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
- [code_inline]: "negateSnd = apsnd uminus"
+ [code_unfold]: "negateSnd = apsnd uminus"
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
--- a/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jul 14 16:27:32 2009 +0200
@@ -24,11 +24,11 @@
lemmas [code del] = char.recs char.cases char.size
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
--- a/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Jul 14 16:27:32 2009 +0200
@@ -26,15 +26,13 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code_inline]:
+lemma zero_nat_code [code, code_unfold_post]:
"0 = (Numeral0 :: nat)"
by simp
-lemmas [code_post] = zero_nat_code [symmetric]
-lemma one_nat_code [code, code_inline]:
+lemma one_nat_code [code, code_unfold_post]:
"1 = (Numeral1 :: nat)"
by simp
-lemmas [code_post] = one_nat_code [symmetric]
lemma Suc_code [code]:
"Suc n = n + 1"
@@ -302,7 +300,7 @@
Natural numerals.
*}
-lemma [code_inline, symmetric, code_post]:
+lemma [code_unfold_post]:
"nat (number_of i) = number_nat_inst.number_of_nat i"
-- {* this interacts as desired with @{thm nat_number_of_def} *}
by (simp add: number_nat_inst.number_of_nat)
@@ -335,9 +333,8 @@
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
unfolding nat_number_of_def number_of_is_id neg_def by simp
-lemma of_nat_int [code_unfold]:
+lemma of_nat_int [code_unfold_post]:
"of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code_post]
code_const int
(SML "_")
--- a/src/HOL/Library/Float.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Float.thy Tue Jul 14 16:27:32 2009 +0200
@@ -42,7 +42,7 @@
instance ..
end
-lemma number_of_float_Float [code_inline, symmetric, code_post]:
+lemma number_of_float_Float [code_unfold_post]:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
--- a/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Tue Jul 14 16:27:32 2009 +0200
@@ -40,10 +40,10 @@
"0 = Fin 0"
definition
- [code_inline]: "1 = Fin 1"
+ [code_unfold]: "1 = Fin 1"
definition
- [code_inline, code del]: "number_of k = Fin (number_of k)"
+ [code_unfold, code del]: "number_of k = Fin (number_of k)"
instance ..
--- a/src/HOL/List.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/List.thy Tue Jul 14 16:27:32 2009 +0200
@@ -3756,7 +3756,7 @@
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
-lemma [code_inline]:
+lemma [code_unfold]:
"eq_class.eq xs [] \<longleftrightarrow> null xs"
by (simp add: eq empty_null)
@@ -3804,7 +3804,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma length_remdups_length_unique [code_inline]:
+lemma length_remdups_length_unique [code_unfold]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all
--- a/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:32 2009 +0200
@@ -20,7 +20,7 @@
begin
definition
- nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
+ nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
instance ..
--- a/src/HOL/Option.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Option.thy Tue Jul 14 16:27:32 2009 +0200
@@ -105,7 +105,7 @@
"is_none x \<longleftrightarrow> x = None"
by (simp add: is_none_def)
-lemma [code_inline]:
+lemma [code_unfold]:
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
--- a/src/HOL/Rational.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/Rational.thy Tue Jul 14 16:27:32 2009 +0200
@@ -1003,7 +1003,7 @@
definition (in term_syntax)
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+ [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/RealDef.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/RealDef.thy Tue Jul 14 16:27:32 2009 +0200
@@ -946,7 +946,7 @@
end
-lemma [code_unfold, symmetric, code_post]:
+lemma [code_unfold_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id real_number_of_def ..
@@ -1129,7 +1129,7 @@
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+ [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/String.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/String.thy Tue Jul 14 16:27:32 2009 +0200
@@ -58,11 +58,11 @@
end
*}
-lemma char_case_nibble_pair [code, code_inline]:
+lemma char_case_nibble_pair [code, code_unfold]:
"char_case f = split f o nibble_pair_of_char"
by (simp add: expand_fun_eq split: char.split)
-lemma char_rec_nibble_pair [code, code_inline]:
+lemma char_rec_nibble_pair [code, code_unfold]:
"char_rec f = split f o nibble_pair_of_char"
unfolding char_case_nibble_pair [symmetric]
by (simp add: expand_fun_eq split: char.split)
--- a/src/HOL/ex/Numeral.thy Tue Jul 14 16:27:31 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Tue Jul 14 16:27:32 2009 +0200
@@ -758,7 +758,7 @@
code_datatype "0::int" Pls Mns
-lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
[simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
by (simp_all add: of_num_less_iff)
-lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code_inline del]
-declare one_is_num_one [code_inline del]
+lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_unfold del]
+declare one_is_num_one [code_unfold del]
hide (open) const sub dup