# HG changeset patch
# User haftmann
# Date 1161333882 -7200
# Node ID 3c5074f028c86154ebc162a02ce667218e3b2790
# Parent  876dd269542363e97f99faeee5998c363fad8e3e
slight cleanup

diff -r 876dd2695423 -r 3c5074f028c8 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Fri Oct 20 10:44:39 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Oct 20 10:44:42 2006 +0200
@@ -13,7 +13,7 @@
 
 instance set :: (eq) eq ..
 
-lemma [code target: Set]:
+lemma [code target: Set, code nofunc]:
   "(A = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
   by blast
 
@@ -240,11 +240,9 @@
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
 
-definition
+definition [code inline]:
   "empty_list = []"
 
-declare empty_list_def [code inline]
-
 lemma [code func]:
   "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
 
diff -r 876dd2695423 -r 3c5074f028c8 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 20 10:44:39 2006 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Oct 20 10:44:42 2006 +0200
@@ -120,22 +120,20 @@
   and vname :: eq
   and mname :: eq
   and ty :: eq
+  and val :: eq
   and instr :: eq ..
 
 definition
   arbitrary_val :: val
-  "arbitrary_val = arbitrary"
+  [symmetric, code inline]: "arbitrary_val = arbitrary"
   arbitrary_cname :: cname
-  "arbitrary_cname = arbitrary"
-
-declare arbitrary_val_def [symmetric, code inline]
-declare arbitrary_cname_def [symmetric, code inline]
+  [symmetric, code inline]: "arbitrary_cname = arbitrary"
 
 definition
   "unit' = Unit"
   "object' = Object"
 
-code_constsubst
+code_axioms
   arbitrary_val \<equiv> unit'
   arbitrary_cname \<equiv> object'
 
@@ -165,7 +163,7 @@
 code_const
   wf_class (SML target_atom "(fn _ => true)")
 
-code_constsubst
+code_axioms
   new_Addr \<equiv> new_addr'
 
 definition