# HG changeset patch
# User wenzelm
# Date 1330277186 -3600
# Node ID 866a798d051cd016a6bdae9e56801b2dd6224a81
# Parent  7f741b2c82a334f6b2d6ab2e867190a04ffcb9e8
tuned proofs;

diff -r 7f741b2c82a3 -r 866a798d051c src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Sun Feb 26 18:25:28 2012 +0100
+++ b/src/HOL/ex/CTL.thy	Sun Feb 26 18:26:26 2012 +0100
@@ -4,7 +4,9 @@
 
 header {* CTL formulae *}
 
-theory CTL imports Main begin
+theory CTL
+imports Main
+begin
 
 text {*
   We formalize basic concepts of Computational Tree Logic (CTL)
@@ -127,19 +129,19 @@
 
 lemma EF_fp: "\<EF> p = p \<union> \<EX> \<EF> p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<union> \<EX> s)" by rule auto
   then show ?thesis by (simp only: EF_def) (rule lfp_unfold)
 qed
 
 lemma AF_fp: "\<AF> p = p \<union> \<AX> \<AF> p"
 proof -
-  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<union> \<AX> s)" by rule auto
   then show ?thesis by (simp only: AF_lfp) (rule lfp_unfold)
 qed
 
 lemma EG_fp: "\<EG> p = p \<inter> \<EX> \<EG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule (auto simp add: EX_def)
+  have "mono (\<lambda>s. p \<inter> \<EX> s)" by rule auto
   then show ?thesis by (simp only: EG_def) (rule gfp_unfold)
 qed
 
@@ -152,7 +154,7 @@
 
 lemma AG_fp: "\<AG> p = p \<inter> \<AX> \<AG> p"
 proof -
-  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule (auto simp add: AX_def EX_def)
+  have "mono (\<lambda>s. p \<inter> \<AX> s)" by rule auto
   then show ?thesis by (simp only: AG_gfp) (rule gfp_unfold)
 qed