# HG changeset patch # User bulwahn # Date 1319188634 -7200 # Node ID d85a2fdc586c655eca2894918eae61c9747cd4e5 # Parent 1b08942bb86ffc91f54ac4798397a71b5daf5550 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Divides.thy Fri Oct 21 11:17:14 2011 +0200 @@ -131,7 +131,7 @@ note that ultimately show thesis by blast qed -lemma dvd_eq_mod_eq_0 [code, code_unfold, code_inline del]: "a dvd b \ b mod a = 0" +lemma dvd_eq_mod_eq_0 [code]: "a dvd b \ b mod a = 0" proof assume "b mod a = 0" with mod_div_equality [of b a] have "b div a * a = b" by simp diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/HOL.thy Fri Oct 21 11:17:14 2011 +0200 @@ -1729,7 +1729,7 @@ assumes equal_eq: "equal x y \ x = y" begin -lemma equal [code_unfold, code_inline del]: "equal = (op =)" +lemma equal: "equal = (op =)" by (rule ext equal_eq)+ lemma equal_refl: "equal x x \ True" diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Oct 21 11:17:14 2011 +0200 @@ -495,7 +495,7 @@ lemma [code_post]: "raise' (STR s) = raise s" unfolding raise'_def by (simp add: STR_inverse) -lemma raise_raise' [code_inline]: +lemma raise_raise' [code_unfold]: "raise s = raise' (STR s)" unfolding raise'_def by (simp add: STR_inverse) diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Executable_Set.thy Fri Oct 21 11:17:14 2011 +0200 @@ -67,7 +67,7 @@ "{} = empty" by simp -lemma [code_unfold, code_inline del]: +lemma "empty = Set []" by simp -- {* Otherwise @{text \}-expansion produces funny things. *} diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Mapping.thy Fri Oct 21 11:17:14 2011 +0200 @@ -90,7 +90,7 @@ subsection {* Properties *} -lemma keys_is_none_lookup [code_inline]: +lemma keys_is_none_lookup [code_unfold]: "k \ keys m \ \ (Option.is_none (lookup m k))" by (auto simp add: keys_def is_none_def) diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Library/Predicate_Compile_Alternative_Defs.thy --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Fri Oct 21 11:17:14 2011 +0200 @@ -84,7 +84,7 @@ definition subtract where - [code_inline]: "subtract x y = y - x" + [code_unfold]: "subtract x y = y - x" setup {* let diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Library/Transitive_Closure_Table.thy --- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Oct 21 11:17:14 2011 +0200 @@ -185,8 +185,6 @@ by (auto simp add: rtranclp_eq_rtrancl_path) qed -declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del] - declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/MicroJava/J/JListExample.thy --- a/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/MicroJava/J/JListExample.thy Fri Oct 21 11:17:14 2011 +0200 @@ -118,12 +118,12 @@ definition undefined_cname :: cname where [code del]: "undefined_cname = undefined" -declare undefined_cname_def[symmetric, code_inline] +declare undefined_cname_def[symmetric, code_unfold] code_datatype Object Xcpt Cname undefined_cname definition undefined_val :: val where [code del]: "undefined_val = undefined" -declare undefined_val_def[symmetric, code_inline] +declare undefined_val_def[symmetric, code_unfold] code_datatype Unit Null Bool Intg Addr undefined_val definition E where diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/MicroJava/J/SystemClasses.thy --- a/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/MicroJava/J/SystemClasses.thy Fri Oct 21 11:17:14 2011 +0200 @@ -13,18 +13,18 @@ *} definition ObjectC :: "'c cdecl" where - [code_inline]: "ObjectC \ (Object, (undefined,[],[]))" + [code_unfold]: "ObjectC \ (Object, (undefined,[],[]))" definition NullPointerC :: "'c cdecl" where - [code_inline]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" + [code_unfold]: "NullPointerC \ (Xcpt NullPointer, (Object,[],[]))" definition ClassCastC :: "'c cdecl" where - [code_inline]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" + [code_unfold]: "ClassCastC \ (Xcpt ClassCast, (Object,[],[]))" definition OutOfMemoryC :: "'c cdecl" where - [code_inline]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" + [code_unfold]: "OutOfMemoryC \ (Xcpt OutOfMemory, (Object,[],[]))" definition SystemClasses :: "'c cdecl list" where - [code_inline]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" + [code_unfold]: "SystemClasses \ [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" end diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Oct 21 11:17:14 2011 +0200 @@ -97,7 +97,7 @@ [inductify] subcls' . -lemma subcls_conv_subcls' [code_inline]: +lemma subcls_conv_subcls' [code_unfold]: "(subcls1 G)^* = (\(C, D). subcls' G C D)" by(simp add: subcls'_def subcls1_def rtrancl_def)(simp add: Collect_def) diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/MicroJava/JVM/JVMListExample.thy --- a/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Fri Oct 21 11:17:14 2011 +0200 @@ -125,11 +125,11 @@ definition undefined_cname :: cname where [code del]: "undefined_cname = undefined" code_datatype Object Xcpt Cname undefined_cname -declare undefined_cname_def[symmetric, code_inline] +declare undefined_cname_def[symmetric, code_unfold] definition undefined_val :: val where [code del]: "undefined_val = undefined" -declare undefined_val_def[symmetric, code_inline] +declare undefined_val_def[symmetric, code_unfold] code_datatype Unit Null Bool Intg Addr undefined_val definition diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Nat.thy Fri Oct 21 11:17:14 2011 +0200 @@ -1301,7 +1301,7 @@ end -declare of_nat_code [code, code_unfold, code_inline del] +declare of_nat_code [code] text{*Class for unital semirings with characteristic zero. Includes non-ordered rings like the complex numbers.*} diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Orderings.thy Fri Oct 21 11:17:14 2011 +0200 @@ -305,13 +305,13 @@ text {* Explicit dictionaries for code generation *} -lemma min_ord_min [code, code_unfold, code_inline del]: +lemma min_ord_min [code]: "min = ord.min (op \)" by (rule ext)+ (simp add: min_def ord.min_def) declare ord.min_def [code] -lemma max_ord_max [code, code_unfold, code_inline del]: +lemma max_ord_max [code]: "max = ord.max (op \)" by (rule ext)+ (simp add: max_def ord.max_def) diff -r 1b08942bb86f -r d85a2fdc586c src/HOL/Power.thy --- a/src/HOL/Power.thy Fri Oct 21 11:17:12 2011 +0200 +++ b/src/HOL/Power.thy Fri Oct 21 11:17:14 2011 +0200 @@ -460,7 +460,7 @@ subsection {* Code generator tweak *} -lemma power_power_power [code, code_unfold, code_inline del]: +lemma power_power_power [code]: "power = power.power (1::'a::{power}) (op *)" unfolding power_def power.power_def ..