src/HOL/Datatype_Examples/Process.thy

--- a/src/HOL/Datatype_Examples/Process.thy	Fri Nov 07 12:24:56 2014 +0100
+++ b/src/HOL/Datatype_Examples/Process.thy	Fri Nov 07 11:28:37 2014 +0100
@@ -17,15 +17,8 @@
 
 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *)
 
-section {* Customization *}
-
 subsection {* Basic properties *}
 
-declare
-  rel_pre_process_def[simp]
-  rel_sum_def[simp]
-  rel_prod_def[simp]
-
 (* Constructors versus discriminators *)
 theorem isAction_isChoice:
 "isAction p \<or> isChoice p"