1.1 --- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 18 17:46:17 2002 +0100
     1.2 +++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 18 18:30:19 2002 +0100
     1.3 @@ -31,7 +31,8 @@
     1.4  This definition allows a succinct statement of the semantics of @{term AF}:
     1.5  \footnote{Do not be misled: neither datatypes nor recursive functions can be
     1.6  extended by new constructors or equations. This is just a trick of the
     1.7 -presentation. In reality one has to define a new datatype and a new function.}
     1.8 +presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
     1.9 +a new datatype and a new function.}
    1.10  *};
    1.11  (*<*)
    1.12  consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
    1.13 @@ -165,7 +166,7 @@
    1.14   "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
    1.15  apply(erule contrapos_np);
    1.16  apply(subst lfp_unfold[OF mono_af]);
    1.17 -apply(simp add:af_def);
    1.18 +apply(simp add: af_def);
    1.19  done;
    1.20  
    1.21  text{*\noindent
    1.22 @@ -210,7 +211,7 @@
    1.23  From this proposition the original goal follows easily:
    1.24  *};
    1.25  
    1.26 - apply(simp add:Paths_def, blast);
    1.27 + apply(simp add: Paths_def, blast);
    1.28  
    1.29  txt{*\noindent
    1.30  The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
    1.31 @@ -242,7 +243,7 @@
    1.32  @{text fast} can prove the base case quickly:
    1.33  *};
    1.34  
    1.35 - apply(fast intro:someI2_ex);
    1.36 + apply(fast intro: someI2_ex);
    1.37  
    1.38  txt{*\noindent
    1.39  What is worth noting here is that we have used \methdx{fast} rather than
    1.40 @@ -285,14 +286,14 @@
    1.41   \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
    1.42  apply(subgoal_tac
    1.43   "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
    1.44 - apply(simp add:Paths_def);
    1.45 + apply(simp add: Paths_def);
    1.46   apply(blast);
    1.47  apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
    1.48  apply(simp);
    1.49  apply(intro strip);
    1.50  apply(induct_tac i);
    1.51   apply(simp);
    1.52 - apply(fast intro:someI2_ex);
    1.53 + apply(fast intro: someI2_ex);
    1.54  apply(simp);
    1.55  apply(rule someI2_ex);
    1.56   apply(blast);
    1.57 @@ -328,7 +329,7 @@
    1.58  Both are solved automatically:
    1.59  *};
    1.60  
    1.61 - apply(auto dest:not_in_lfp_afD);
    1.62 + apply(auto dest: not_in_lfp_afD);
    1.63  done;
    1.64  
    1.65  text{*
    1.66 @@ -388,7 +389,7 @@
    1.67  
    1.68  lemma "lfp(eufix A B) \<subseteq> eusem A B"
    1.69  apply(rule lfp_lowerbound)
    1.70 -apply(clarsimp simp add:eusem_def eufix_def);
    1.71 +apply(clarsimp simp add: eusem_def eufix_def);
    1.72  apply(erule disjE);
    1.73   apply(rule_tac x = "[]" in exI);
    1.74   apply simp
    1.75 @@ -403,15 +404,15 @@
    1.76  done
    1.77  
    1.78  lemma "eusem A B \<subseteq> lfp(eufix A B)";
    1.79 -apply(clarsimp simp add:eusem_def);
    1.80 +apply(clarsimp simp add: eusem_def);
    1.81  apply(erule rev_mp);
    1.82  apply(rule_tac x = x in spec);
    1.83  apply(induct_tac p);
    1.84   apply(subst lfp_unfold[OF mono_eufix])
    1.85 - apply(simp add:eufix_def);
    1.86 + apply(simp add: eufix_def);
    1.87  apply(clarsimp);
    1.88  apply(subst lfp_unfold[OF mono_eufix])
    1.89 -apply(simp add:eufix_def);
    1.90 +apply(simp add: eufix_def);
    1.91  apply blast;
    1.92  done
    1.93  
    1.94 @@ -429,7 +430,7 @@
    1.95  "apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
    1.96  
    1.97  lemma [iff]: "apath s \<in> Paths s";
    1.98 -apply(simp add:Paths_def);
    1.99 +apply(simp add: Paths_def);
   1.100  apply(blast intro: M_total[THEN someI_ex])
   1.101  done
   1.102  
   1.103 @@ -438,11 +439,11 @@
   1.104  "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
   1.105  
   1.106  lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
   1.107 -by(simp add:Paths_def pcons_def split:nat.split);
   1.108 +by(simp add: Paths_def pcons_def split: nat.split);
   1.109  
   1.110  lemma "lfp(eufix A B) \<subseteq> eusem A B"
   1.111  apply(rule lfp_lowerbound)
   1.112 -apply(clarsimp simp add:eusem_def eufix_def);
   1.113 +apply(clarsimp simp add: eusem_def eufix_def);
   1.114  apply(erule disjE);
   1.115   apply(rule_tac x = "apath x" in bexI);
   1.116    apply(rule_tac x = 0 in exI);
   1.117 @@ -451,8 +452,8 @@
   1.118  apply(clarify);
   1.119  apply(rule_tac x = "pcons xb p" in bexI);
   1.120   apply(rule_tac x = "j+1" in exI);
   1.121 - apply (simp add:pcons_def split:nat.split);
   1.122 -apply (simp add:pcons_PathI)
   1.123 + apply (simp add: pcons_def split: nat.split);
   1.124 +apply (simp add: pcons_PathI)
   1.125  done
   1.126  *)
   1.127  (*>*)