# HG changeset patch
# User traytel
# Date 1347263841 -7200
# Node ID fd11fe9dc6bb0ed4ed0d40131efeb167829febd9
# Parent  f7e75b802ef25d37d7710e6728e3815043310eed
simplify "Process" example even further

diff -r f7e75b802ef2 -r fd11fe9dc6bb src/HOL/Codatatype/Examples/Process.thy
--- a/src/HOL/Codatatype/Examples/Process.thy	Mon Sep 10 09:56:06 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy	Mon Sep 10 09:57:21 2012 +0200
@@ -19,16 +19,6 @@
 
 section {* Customization *}
 
-subsection{* Setup for map, set, pred  *}
-
-lemma pre_process_pred[simp]:
-"pre_process_pred (op =) \<phi> (Inl (a,p)) (Inl (a',p')) \<longleftrightarrow> a = a' \<and> \<phi> p p'"
-"pre_process_pred (op =) \<phi> (Inr (p,q)) (Inr (p',q')) \<longleftrightarrow> \<phi> p p' \<and> \<phi> q q'"
-"\<not> pre_process_pred (op =) \<phi> (Inl ap) (Inr q1q2)"
-"\<not> pre_process_pred (op =) \<phi> (Inr q1q2) (Inl ap)"
-by (auto simp: diag_def pre_process.pred_unfold)
-
-
 subsection {* Basic properties *}
 
 declare
@@ -37,6 +27,7 @@
   process.discs[simp]
   process.sels[simp]
   process.collapse[simp]
+  pre_process.pred_unfold[simp]
 
 lemmas process_exhaust =
   process.exhaust[elim, case_names Action Choice]