squash style: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>

lib/concurrency/examples/Peterson_Atomicity.thy

@@ -139,7 +139,7 @@ text \<open>
   either we're in the critical section or waiting to enter with priority.\<close>
 abbreviation (input) enabled :: "ident \<Rightarrow> ('a, 'b) p_state \<Rightarrow> bool" where
   "enabled ident s \<equiv>
-     (critical (ab_label s ident) \<or> (ab_label s ident = Awaiting \<and> t_v s = ident))"
+     critical (ab_label s ident) \<or> ab_label s ident = Awaiting \<and> t_v s = ident"
 
 definition key_peterson_inv :: "('a, 'b) p_state \<Rightarrow> bool" where
   "key_peterson_inv s = (\<not> (enabled A s \<and> enabled B s))"
@@ -182,8 +182,8 @@ lemma reflp_peterson_rel[simp]:
 declare reflp_peterson_rel[THEN reflpD, simp]
 
 lemma peterson_rel_imp_assume_invs:
-  "\<lbrakk>invs x; (peterson_rel ident x y \<and> invs x \<and> invs y \<longrightarrow> P x y)\<rbrakk>
-   \<Longrightarrow> (peterson_rel ident x y \<longrightarrow> P x y)"
+  "\<lbrakk>invs x; peterson_rel ident x y \<and> invs x \<and> invs y \<longrightarrow> P x y\<rbrakk>
+   \<Longrightarrow> peterson_rel ident x y \<longrightarrow> P x y"
   by (simp add: peterson_rel_def)
 
 end