eliminated spurious semicolons;
authorwenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860fee7cfa69c50
parent 58859 d5ff8b782b29
child 58861 5ff61774df11
eliminated spurious semicolons;
src/Doc/Logics_ZF/ZF_examples.thy
src/Doc/Prog_Prove/Types_and_funs.thy
src/Doc/Tutorial/Advanced/Partial.thy
src/Doc/Tutorial/CTL/Base.thy
src/Doc/Tutorial/CTL/CTL.thy
src/Doc/Tutorial/CTL/CTLind.thy
src/Doc/Tutorial/CodeGen/CodeGen.thy
src/Doc/Tutorial/Datatype/ABexpr.thy
src/Doc/Tutorial/Datatype/Fundata.thy
src/Doc/Tutorial/Datatype/Nested.thy
src/Doc/Tutorial/Datatype/unfoldnested.thy
src/Doc/Tutorial/Fun/fun0.thy
src/Doc/Tutorial/Ifexpr/Ifexpr.thy
src/Doc/Tutorial/Inductive/Star.thy
src/Doc/Tutorial/Misc/AdvancedInd.thy
src/Doc/Tutorial/Misc/Itrev.thy
src/Doc/Tutorial/Misc/Option2.thy
src/Doc/Tutorial/Misc/Tree.thy
src/Doc/Tutorial/Misc/Tree2.thy
src/Doc/Tutorial/Misc/case_exprs.thy
src/Doc/Tutorial/Misc/fakenat.thy
src/Doc/Tutorial/Misc/pairs2.thy
src/Doc/Tutorial/Misc/prime_def.thy
src/Doc/Tutorial/Protocol/Event.thy
src/Doc/Tutorial/Protocol/Message.thy
src/Doc/Tutorial/Recdef/Induction.thy
src/Doc/Tutorial/Recdef/examples.thy
src/Doc/Tutorial/Recdef/simplification.thy
src/Doc/Tutorial/Rules/Blast.thy
src/Doc/Tutorial/Rules/Force.thy
src/Doc/Tutorial/Rules/Forward.thy
src/Doc/Tutorial/Rules/TPrimes.thy
src/Doc/Tutorial/Sets/Functions.thy
src/Doc/Tutorial/Sets/Relations.thy
src/Doc/Tutorial/ToyList/ToyList.thy
src/Doc/Tutorial/Trie/Trie.thy
src/Doc/Tutorial/Types/Numbers.thy
src/Doc/Tutorial/Types/Pairs.thy
src/FOLP/ex/Classical.thy
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Module.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/Comp/TypeInf.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/DFA/Kildall.thy
src/HOL/MicroJava/DFA/Listn.thy
src/HOL/MicroJava/DFA/Opt.thy
src/HOL/MicroJava/DFA/Product.thy
src/HOL/MicroJava/DFA/Semilat.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/NSA/CLim.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/UNITY/Comp/PriorityAux.thy
src/Pure/Pure.thy
src/Sequents/LK0.thy
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/WO2_AC16.thy
src/ZF/Arith.thy
src/ZF/Coind/Values.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Rank.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Epsilon.thy
src/ZF/List_ZF.thy
src/ZF/Nat_ZF.thy
src/ZF/OrdQuant.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/ClientImpl.thy
src/ZF/Univ.thy
src/ZF/equalities.thy
src/ZF/ex/Group.thy
src/ZF/ex/LList.thy
src/ZF/func.thy
     1.1 --- a/src/Doc/Logics_ZF/ZF_examples.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Logics_ZF/ZF_examples.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5  text {*
     1.6  @{thm[display] Br_in_bt[no_vars]}
     1.7 -*};
     1.8 +*}
     1.9  
    1.10  subsection{*Primitive recursion*}
    1.11  
    1.12 @@ -92,7 +92,7 @@
    1.13  
    1.14  
    1.15  consts
    1.16 -  llist  :: "i=>i";
    1.17 +  llist  :: "i=>i"
    1.18  
    1.19  codatatype
    1.20    "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
     2.1 --- a/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 11:40:55 2014 +0100
     2.2 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Sat Nov 01 14:20:38 2014 +0100
     2.3 @@ -298,8 +298,8 @@
     2.4  \end{quote}
     2.5  Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is
     2.6  just not true.  The correct generalization is
     2.7 -*};
     2.8 -(*<*)oops;(*>*)
     2.9 +*}
    2.10 +(*<*)oops(*>*)
    2.11  lemma "itrev xs ys = rev xs @ ys"
    2.12  (*<*)apply(induction xs, auto)(*>*)
    2.13  txt{*
     3.1 --- a/src/Doc/Tutorial/Advanced/Partial.thy	Sat Nov 01 11:40:55 2014 +0100
     3.2 +++ b/src/Doc/Tutorial/Advanced/Partial.thy	Sat Nov 01 14:20:38 2014 +0100
     3.3 @@ -138,7 +138,7 @@
     3.4  *}
     3.5  
     3.6  lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
     3.7 -apply(induct_tac f x rule: find.induct);
     3.8 +apply(induct_tac f x rule: find.induct)
     3.9  apply simp
    3.10  done
    3.11  
    3.12 @@ -191,7 +191,7 @@
    3.13    \<exists>y. while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x) = (y,y) \<and>
    3.14         f y = y"
    3.15  apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
    3.16 -               r = "inv_image (step1 f) fst" in while_rule);
    3.17 +               r = "inv_image (step1 f) fst" in while_rule)
    3.18  apply auto
    3.19  apply(simp add: inv_image_def step1_def)
    3.20  done
     4.1 --- a/src/Doc/Tutorial/CTL/Base.thy	Sat Nov 01 11:40:55 2014 +0100
     4.2 +++ b/src/Doc/Tutorial/CTL/Base.thy	Sat Nov 01 14:20:38 2014 +0100
     4.3 @@ -69,7 +69,7 @@
     4.4  transition system, i.e.\ a relation between states:
     4.5  *}
     4.6  
     4.7 -consts M :: "(state \<times> state)set";
     4.8 +consts M :: "(state \<times> state)set"
     4.9  
    4.10  text{*\noindent
    4.11  This is Isabelle's way of declaring a constant without defining it.
     5.1 --- a/src/Doc/Tutorial/CTL/CTL.thy	Sat Nov 01 11:40:55 2014 +0100
     5.2 +++ b/src/Doc/Tutorial/CTL/CTL.thy	Sat Nov 01 14:20:38 2014 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  (*<*)theory CTL imports Base begin(*>*)
     5.5  
     5.6 -subsection{*Computation Tree Logic --- CTL*};
     5.7 +subsection{*Computation Tree Logic --- CTL*}
     5.8  
     5.9  text{*\label{sec:CTL}
    5.10  \index{CTL|(}%
    5.11 @@ -8,21 +8,21 @@
    5.12  Let us be adventurous and introduce a more expressive temporal operator.
    5.13  We extend the datatype
    5.14  @{text formula} by a new constructor
    5.15 -*};
    5.16 +*}
    5.17  (*<*)
    5.18  datatype formula = Atom "atom"
    5.19                    | Neg formula
    5.20                    | And formula formula
    5.21                    | AX formula
    5.22                    | EF formula(*>*)
    5.23 -                  | AF formula;
    5.24 +                  | AF formula
    5.25  
    5.26  text{*\noindent
    5.27  which stands for ``\emph{A}lways in the \emph{F}uture'':
    5.28  on all infinite paths, at some point the formula holds.
    5.29  Formalizing the notion of an infinite path is easy
    5.30  in HOL: it is simply a function from @{typ nat} to @{typ state}.
    5.31 -*};
    5.32 +*}
    5.33  
    5.34  definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where
    5.35  "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}"
    5.36 @@ -33,7 +33,7 @@
    5.37  extended by new constructors or equations. This is just a trick of the
    5.38  presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
    5.39  a new datatype and a new function.}
    5.40 -*};
    5.41 +*}
    5.42  (*<*)
    5.43  primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where
    5.44  "s \<Turnstile> Atom a  =  (a \<in> L s)" |
    5.45 @@ -47,7 +47,7 @@
    5.46  text{*\noindent
    5.47  Model checking @{const AF} involves a function which
    5.48  is just complicated enough to warrant a separate definition:
    5.49 -*};
    5.50 +*}
    5.51  
    5.52  definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
    5.53  "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}"
    5.54 @@ -55,7 +55,7 @@
    5.55  text{*\noindent
    5.56  Now we define @{term "mc(AF f)"} as the least set @{term T} that includes
    5.57  @{term"mc f"} and all states all of whose direct successors are in @{term T}:
    5.58 -*};
    5.59 +*}
    5.60  (*<*)
    5.61  primrec mc :: "formula \<Rightarrow> state set" where
    5.62  "mc(Atom a)  = {s. a \<in> L s}" |
    5.63 @@ -63,45 +63,45 @@
    5.64  "mc(And f g) = mc f \<inter> mc g" |
    5.65  "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}" |
    5.66  "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M\<inverse> `` T)"|(*>*)
    5.67 -"mc(AF f)    = lfp(af(mc f))";
    5.68 +"mc(AF f)    = lfp(af(mc f))"
    5.69  
    5.70  text{*\noindent
    5.71  Because @{const af} is monotone in its second argument (and also its first, but
    5.72  that is irrelevant), @{term"af A"} has a least fixed point:
    5.73 -*};
    5.74 +*}
    5.75  
    5.76 -lemma mono_af: "mono(af A)";
    5.77 -apply(simp add: mono_def af_def);
    5.78 -apply blast;
    5.79 +lemma mono_af: "mono(af A)"
    5.80 +apply(simp add: mono_def af_def)
    5.81 +apply blast
    5.82  done
    5.83  (*<*)
    5.84 -lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)";
    5.85 -apply(rule monoI);
    5.86 -by(blast);
    5.87 +lemma mono_ef: "mono(\<lambda>T. A \<union> M\<inverse> `` T)"
    5.88 +apply(rule monoI)
    5.89 +by(blast)
    5.90  
    5.91  lemma EF_lemma:
    5.92 -  "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}";
    5.93 -apply(rule equalityI);
    5.94 - apply(rule subsetI);
    5.95 - apply(simp);
    5.96 - apply(erule lfp_induct_set);
    5.97 -  apply(rule mono_ef);
    5.98 - apply(simp);
    5.99 - apply(blast intro: rtrancl_trans);
   5.100 -apply(rule subsetI);
   5.101 -apply(simp, clarify);
   5.102 -apply(erule converse_rtrancl_induct);
   5.103 - apply(subst lfp_unfold[OF mono_ef]);
   5.104 - apply(blast);
   5.105 -apply(subst lfp_unfold[OF mono_ef]);
   5.106 -by(blast);
   5.107 +  "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
   5.108 +apply(rule equalityI)
   5.109 + apply(rule subsetI)
   5.110 + apply(simp)
   5.111 + apply(erule lfp_induct_set)
   5.112 +  apply(rule mono_ef)
   5.113 + apply(simp)
   5.114 + apply(blast intro: rtrancl_trans)
   5.115 +apply(rule subsetI)
   5.116 +apply(simp, clarify)
   5.117 +apply(erule converse_rtrancl_induct)
   5.118 + apply(subst lfp_unfold[OF mono_ef])
   5.119 + apply(blast)
   5.120 +apply(subst lfp_unfold[OF mono_ef])
   5.121 +by(blast)
   5.122  (*>*)
   5.123  text{*
   5.124  All we need to prove now is  @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states
   5.125  that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@.
   5.126  This time we prove the two inclusions separately, starting
   5.127  with the easy one:
   5.128 -*};
   5.129 +*}
   5.130  
   5.131  theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}"
   5.132  
   5.133 @@ -114,9 +114,9 @@
   5.134  \end{center}
   5.135  The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
   5.136  a decision that \isa{auto} takes for us:
   5.137 -*};
   5.138 -apply(rule lfp_lowerbound);
   5.139 -apply(auto simp add: af_def Paths_def);
   5.140 +*}
   5.141 +apply(rule lfp_lowerbound)
   5.142 +apply(auto simp add: af_def Paths_def)
   5.143  
   5.144  txt{*
   5.145  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
   5.146 @@ -124,11 +124,11 @@
   5.147  The rest is automatic, which is surprising because it involves
   5.148  finding the instantiation @{term"\<lambda>i::nat. p(i+1)"}
   5.149  for @{text"\<forall>p"}.
   5.150 -*};
   5.151 +*}
   5.152  
   5.153 -apply(erule_tac x = "p 1" in allE);
   5.154 -apply(auto);
   5.155 -done;
   5.156 +apply(erule_tac x = "p 1" in allE)
   5.157 +apply(auto)
   5.158 +done
   5.159  
   5.160  
   5.161  text{*
   5.162 @@ -143,14 +143,14 @@
   5.163  
   5.164  The one-step argument in the sketch above
   5.165  is proved by a variant of contraposition:
   5.166 -*};
   5.167 +*}
   5.168  
   5.169  lemma not_in_lfp_afD:
   5.170 - "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
   5.171 -apply(erule contrapos_np);
   5.172 -apply(subst lfp_unfold[OF mono_af]);
   5.173 -apply(simp add: af_def);
   5.174 -done;
   5.175 + "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"
   5.176 +apply(erule contrapos_np)
   5.177 +apply(subst lfp_unfold[OF mono_af])
   5.178 +apply(simp add: af_def)
   5.179 +done
   5.180  
   5.181  text{*\noindent
   5.182  We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}.
   5.183 @@ -159,7 +159,7 @@
   5.184  
   5.185  Now we iterate this process. The following construction of the desired
   5.186  path is parameterized by a predicate @{term Q} that should hold along the path:
   5.187 -*};
   5.188 +*}
   5.189  
   5.190  primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where
   5.191  "path s Q 0 = s" |
   5.192 @@ -175,41 +175,41 @@
   5.193  
   5.194  Let us show that if each state @{term s} that satisfies @{term Q}
   5.195  has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path:
   5.196 -*};
   5.197 +*}
   5.198  
   5.199  lemma infinity_lemma:
   5.200    "\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow>
   5.201 -   \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
   5.202 +   \<exists>p\<in>Paths s. \<forall>i. Q(p i)"
   5.203  
   5.204  txt{*\noindent
   5.205  First we rephrase the conclusion slightly because we need to prove simultaneously
   5.206  both the path property and the fact that @{term Q} holds:
   5.207 -*};
   5.208 +*}
   5.209  
   5.210  apply(subgoal_tac
   5.211 -  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))");
   5.212 +  "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))")
   5.213  
   5.214  txt{*\noindent
   5.215  From this proposition the original goal follows easily:
   5.216 -*};
   5.217 +*}
   5.218  
   5.219 - apply(simp add: Paths_def, blast);
   5.220 + apply(simp add: Paths_def, blast)
   5.221  
   5.222  txt{*\noindent
   5.223  The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
   5.224 -*};
   5.225 +*}
   5.226  
   5.227 -apply(rule_tac x = "path s Q" in exI);
   5.228 -apply(clarsimp);
   5.229 +apply(rule_tac x = "path s Q" in exI)
   5.230 +apply(clarsimp)
   5.231  
   5.232  txt{*\noindent
   5.233  After simplification and clarification, the subgoal has the following form:
   5.234  @{subgoals[display,indent=0,margin=70,goals_limit=1]}
   5.235  It invites a proof by induction on @{term i}:
   5.236 -*};
   5.237 +*}
   5.238  
   5.239 -apply(induct_tac i);
   5.240 - apply(simp);
   5.241 +apply(induct_tac i)
   5.242 + apply(simp)
   5.243  
   5.244  txt{*\noindent
   5.245  After simplification, the base case boils down to
   5.246 @@ -223,9 +223,9 @@
   5.247  two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and
   5.248  @{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
   5.249  @{text fast} can prove the base case quickly:
   5.250 -*};
   5.251 +*}
   5.252  
   5.253 - apply(fast intro: someI2_ex);
   5.254 + apply(fast intro: someI2_ex)
   5.255  
   5.256  txt{*\noindent
   5.257  What is worth noting here is that we have used \methdx{fast} rather than
   5.258 @@ -242,15 +242,15 @@
   5.259  occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
   5.260  solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
   5.261  show the proof commands but do not describe the details:
   5.262 -*};
   5.263 +*}
   5.264  
   5.265 -apply(simp);
   5.266 -apply(rule someI2_ex);
   5.267 - apply(blast);
   5.268 -apply(rule someI2_ex);
   5.269 - apply(blast);
   5.270 -apply(blast);
   5.271 -done;
   5.272 +apply(simp)
   5.273 +apply(rule someI2_ex)
   5.274 + apply(blast)
   5.275 +apply(rule someI2_ex)
   5.276 + apply(blast)
   5.277 +apply(blast)
   5.278 +done
   5.279  
   5.280  text{*
   5.281  Function @{const path} has fulfilled its purpose now and can be forgotten.
   5.282 @@ -261,58 +261,58 @@
   5.283  @{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}
   5.284  is extensionally equal to @{term"path s Q"},
   5.285  where @{term rec_nat} is the predefined primitive recursor on @{typ nat}.
   5.286 -*};
   5.287 +*}
   5.288  (*<*)
   5.289  lemma
   5.290  "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>
   5.291 - \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
   5.292 + \<exists> p\<in>Paths s. \<forall> i. Q(p i)"
   5.293  apply(subgoal_tac
   5.294 - "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
   5.295 - apply(simp add: Paths_def);
   5.296 - apply(blast);
   5.297 -apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
   5.298 -apply(simp);
   5.299 -apply(intro strip);
   5.300 -apply(induct_tac i);
   5.301 - apply(simp);
   5.302 - apply(fast intro: someI2_ex);
   5.303 -apply(simp);
   5.304 -apply(rule someI2_ex);
   5.305 - apply(blast);
   5.306 -apply(rule someI2_ex);
   5.307 - apply(blast);
   5.308 -by(blast);
   5.309 + "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))")
   5.310 + apply(simp add: Paths_def)
   5.311 + apply(blast)
   5.312 +apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI)
   5.313 +apply(simp)
   5.314 +apply(intro strip)
   5.315 +apply(induct_tac i)
   5.316 + apply(simp)
   5.317 + apply(fast intro: someI2_ex)
   5.318 +apply(simp)
   5.319 +apply(rule someI2_ex)
   5.320 + apply(blast)
   5.321 +apply(rule someI2_ex)
   5.322 + apply(blast)
   5.323 +by(blast)
   5.324  (*>*)
   5.325  
   5.326  text{*
   5.327  At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
   5.328 -*};
   5.329 +*}
   5.330  
   5.331 -theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)";
   5.332 +theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)"
   5.333  
   5.334  txt{*\noindent
   5.335  The proof is again pointwise and then by contraposition:
   5.336 -*};
   5.337 +*}
   5.338  
   5.339 -apply(rule subsetI);
   5.340 -apply(erule contrapos_pp);
   5.341 -apply simp;
   5.342 +apply(rule subsetI)
   5.343 +apply(erule contrapos_pp)
   5.344 +apply simp
   5.345  
   5.346  txt{*
   5.347  @{subgoals[display,indent=0,goals_limit=1]}
   5.348  Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
   5.349  premise of @{thm[source]infinity_lemma} and the original subgoal:
   5.350 -*};
   5.351 +*}
   5.352  
   5.353 -apply(drule infinity_lemma);
   5.354 +apply(drule infinity_lemma)
   5.355  
   5.356  txt{*
   5.357  @{subgoals[display,indent=0,margin=65]}
   5.358  Both are solved automatically:
   5.359 -*};
   5.360 +*}
   5.361  
   5.362 - apply(auto dest: not_in_lfp_afD);
   5.363 -done;
   5.364 + apply(auto dest: not_in_lfp_afD)
   5.365 +done
   5.366  
   5.367  text{*
   5.368  If you find these proofs too complicated, we recommend that you read
   5.369 @@ -324,9 +324,9 @@
   5.370  @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
   5.371  *}
   5.372  
   5.373 -theorem "mc f = {s. s \<Turnstile> f}";
   5.374 -apply(induct_tac f);
   5.375 -apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
   5.376 +theorem "mc f = {s. s \<Turnstile> f}"
   5.377 +apply(induct_tac f)
   5.378 +apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
   5.379  done
   5.380  
   5.381  text{*
   5.382 @@ -377,22 +377,22 @@
   5.383  apply simp
   5.384  done
   5.385  
   5.386 -lemma mono_eufix: "mono(eufix A B)";
   5.387 -apply(simp add: mono_def eufix_def);
   5.388 -apply blast;
   5.389 +lemma mono_eufix: "mono(eufix A B)"
   5.390 +apply(simp add: mono_def eufix_def)
   5.391 +apply blast
   5.392  done
   5.393  
   5.394 -lemma "eusem A B \<subseteq> lfp(eufix A B)";
   5.395 -apply(clarsimp simp add: eusem_def);
   5.396 -apply(erule rev_mp);
   5.397 -apply(rule_tac x = x in spec);
   5.398 -apply(induct_tac p);
   5.399 +lemma "eusem A B \<subseteq> lfp(eufix A B)"
   5.400 +apply(clarsimp simp add: eusem_def)
   5.401 +apply(erule rev_mp)
   5.402 +apply(rule_tac x = x in spec)
   5.403 +apply(induct_tac p)
   5.404   apply(subst lfp_unfold[OF mono_eufix])
   5.405 - apply(simp add: eufix_def);
   5.406 -apply(clarsimp);
   5.407 + apply(simp add: eufix_def)
   5.408 +apply(clarsimp)
   5.409  apply(subst lfp_unfold[OF mono_eufix])
   5.410 -apply(simp add: eufix_def);
   5.411 -apply blast;
   5.412 +apply(simp add: eufix_def)
   5.413 +apply blast
   5.414  done
   5.415  
   5.416  (*
     6.1 --- a/src/Doc/Tutorial/CTL/CTLind.thy	Sat Nov 01 11:40:55 2014 +0100
     6.2 +++ b/src/Doc/Tutorial/CTL/CTLind.thy	Sat Nov 01 14:20:38 2014 +0100
     6.3 @@ -29,7 +29,7 @@
     6.4    for s :: state and A :: "state set"
     6.5  where
     6.6      "s \<in> Avoid s A"
     6.7 -  | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A";
     6.8 +  | "\<lbrakk> t \<in> Avoid s A; t \<notin> A; (t,u) \<in> M \<rbrakk> \<Longrightarrow> u \<in> Avoid s A"
     6.9  
    6.10  text{*
    6.11  It is easy to see that for any infinite @{term A}-avoiding path @{term f}
    6.12 @@ -44,12 +44,12 @@
    6.13  
    6.14  lemma ex_infinite_path[rule_format]:
    6.15    "t \<in> Avoid s A  \<Longrightarrow>
    6.16 -   \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)";
    6.17 -apply(erule Avoid.induct);
    6.18 - apply(blast);
    6.19 -apply(clarify);
    6.20 -apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
    6.21 -apply(simp_all add: Paths_def split: nat.split);
    6.22 +   \<forall>f\<in>Paths t. (\<forall>i. f i \<notin> A) \<longrightarrow> (\<exists>p\<in>Paths s. \<forall>i. p i \<notin> A)"
    6.23 +apply(erule Avoid.induct)
    6.24 + apply(blast)
    6.25 +apply(clarify)
    6.26 +apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec)
    6.27 +apply(simp_all add: Paths_def split: nat.split)
    6.28  done
    6.29  
    6.30  text{*\noindent
    6.31 @@ -69,7 +69,7 @@
    6.32  *}
    6.33  
    6.34  lemma Avoid_in_lfp[rule_format(no_asm)]:
    6.35 -  "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
    6.36 +  "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)"
    6.37  
    6.38  txt{*\noindent
    6.39  The proof is by induction on the ``distance'' between @{term t} and @{term
    6.40 @@ -87,9 +87,9 @@
    6.41  moment we assume this and proceed with the induction:
    6.42  *}
    6.43  
    6.44 -apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}");
    6.45 - apply(erule_tac a = t in wf_induct);
    6.46 - apply(clarsimp);
    6.47 +apply(subgoal_tac "wf{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> x \<notin> A}")
    6.48 + apply(erule_tac a = t in wf_induct)
    6.49 + apply(clarsimp)
    6.50  (*<*)apply(rename_tac t)(*>*)
    6.51  
    6.52  txt{*\noindent
    6.53 @@ -106,9 +106,9 @@
    6.54  @{term"lfp(af A)"}. Mechanically:
    6.55  *}
    6.56  
    6.57 - apply(subst lfp_unfold[OF mono_af]);
    6.58 - apply(simp (no_asm) add: af_def);
    6.59 - apply(blast intro: Avoid.intros);
    6.60 + apply(subst lfp_unfold[OF mono_af])
    6.61 + apply(simp (no_asm) add: af_def)
    6.62 + apply(blast intro: Avoid.intros)
    6.63  
    6.64  txt{*
    6.65  Having proved the main goal, we return to the proof obligation that the 
    6.66 @@ -121,11 +121,11 @@
    6.67  @{term A}-avoiding path starting in @{term s} follows, contradiction.
    6.68  *}
    6.69  
    6.70 -apply(erule contrapos_pp);
    6.71 -apply(simp add: wf_iff_no_infinite_down_chain);
    6.72 -apply(erule exE);
    6.73 -apply(rule ex_infinite_path);
    6.74 -apply(auto simp add: Paths_def);
    6.75 +apply(erule contrapos_pp)
    6.76 +apply(simp add: wf_iff_no_infinite_down_chain)
    6.77 +apply(erule exE)
    6.78 +apply(rule ex_infinite_path)
    6.79 +apply(auto simp add: Paths_def)
    6.80  done
    6.81  
    6.82  text{*
    6.83 @@ -141,8 +141,8 @@
    6.84  by the first @{const Avoid}-rule. Isabelle confirms this:%
    6.85  \index{CTL|)}*}
    6.86  
    6.87 -theorem AF_lemma2:  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
    6.88 -by(auto elim: Avoid_in_lfp intro: Avoid.intros);
    6.89 +theorem AF_lemma2:  "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)"
    6.90 +by(auto elim: Avoid_in_lfp intro: Avoid.intros)
    6.91  
    6.92  
    6.93  (*<*)end(*>*)
     7.1 --- a/src/Doc/Tutorial/CodeGen/CodeGen.thy	Sat Nov 01 11:40:55 2014 +0100
     7.2 +++ b/src/Doc/Tutorial/CodeGen/CodeGen.thy	Sat Nov 01 14:20:38 2014 +0100
     7.3 @@ -15,10 +15,10 @@
     7.4  appropriate function itself.
     7.5  *}
     7.6  
     7.7 -type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
     7.8 +type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
     7.9  datatype (dead 'a, 'v) expr = Cex 'v
    7.10                        | Vex 'a
    7.11 -                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
    7.12 +                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr"
    7.13  
    7.14  text{*\noindent
    7.15  The three constructors represent constants, variables and the application of
    7.16 @@ -42,7 +42,7 @@
    7.17  
    7.18  datatype (dead 'a, 'v) instr = Const 'v
    7.19                         | Load 'a
    7.20 -                       | Apply "'v binop";
    7.21 +                       | Apply "'v binop"
    7.22  
    7.23  text{*
    7.24  The execution of the stack machine is modelled by a function
    7.25 @@ -83,22 +83,22 @@
    7.26  Now we have to prove the correctness of the compiler, i.e.\ that the
    7.27  execution of a compiled expression results in the value of the expression:
    7.28  *}
    7.29 -theorem "exec (compile e) s [] = [value e s]";
    7.30 -(*<*)oops;(*>*)
    7.31 +theorem "exec (compile e) s [] = [value e s]"
    7.32 +(*<*)oops(*>*)
    7.33  text{*\noindent
    7.34  This theorem needs to be generalized:
    7.35  *}
    7.36  
    7.37 -theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
    7.38 +theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
    7.39  
    7.40  txt{*\noindent
    7.41  It will be proved by induction on @{term"e"} followed by simplification.  
    7.42  First, we must prove a lemma about executing the concatenation of two
    7.43  instruction sequences:
    7.44  *}
    7.45 -(*<*)oops;(*>*)
    7.46 +(*<*)oops(*>*)
    7.47  lemma exec_app[simp]:
    7.48 -  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    7.49 +  "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 
    7.50  
    7.51  txt{*\noindent
    7.52  This requires induction on @{term"xs"} and ordinary simplification for the
    7.53 @@ -106,7 +106,7 @@
    7.54  that contains two @{text"case"}-expressions over instructions. Thus we add
    7.55  automatic case splitting, which finishes the proof:
    7.56  *}
    7.57 -apply(induct_tac xs, simp, simp split: instr.split);
    7.58 +apply(induct_tac xs, simp, simp split: instr.split)
    7.59  (*<*)done(*>*)
    7.60  text{*\noindent
    7.61  Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can
    7.62 @@ -114,10 +114,10 @@
    7.63  rewritten as
    7.64  *}
    7.65  (*<*)
    7.66 -declare exec_app[simp del];
    7.67 -lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    7.68 +declare exec_app[simp del]
    7.69 +lemma [simp]: "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)" 
    7.70  (*>*)
    7.71 -apply(induct_tac xs, simp_all split: instr.split);
    7.72 +apply(induct_tac xs, simp_all split: instr.split)
    7.73  (*<*)done(*>*)
    7.74  text{*\noindent
    7.75  Although this is more compact, it is less clear for the reader of the proof.
    7.76 @@ -129,7 +129,7 @@
    7.77  \index{compiling expressions example|)}
    7.78  *}
    7.79  (*<*)
    7.80 -theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
    7.81 -by(induct_tac e, auto);
    7.82 +theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs"
    7.83 +by(induct_tac e, auto)
    7.84  end
    7.85  (*>*)
     8.1 --- a/src/Doc/Tutorial/Datatype/ABexpr.thy	Sat Nov 01 11:40:55 2014 +0100
     8.2 +++ b/src/Doc/Tutorial/Datatype/ABexpr.thy	Sat Nov 01 14:20:38 2014 +0100
     8.3 @@ -1,5 +1,5 @@
     8.4  (*<*)
     8.5 -theory ABexpr imports Main begin;
     8.6 +theory ABexpr imports Main begin
     8.7  (*>*)
     8.8  
     8.9  text{*
    8.10 @@ -24,7 +24,7 @@
    8.11                   | Num nat
    8.12  and      'a bexp = Less "'a aexp" "'a aexp"
    8.13                   | And  "'a bexp" "'a bexp"
    8.14 -                 | Neg  "'a bexp";
    8.15 +                 | Neg  "'a bexp"
    8.16  
    8.17  text{*\noindent
    8.18  Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
    8.19 @@ -92,13 +92,13 @@
    8.20  *}
    8.21  
    8.22  lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env) \<and>
    8.23 -        evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)";
    8.24 -apply(induct_tac a and b);
    8.25 +        evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
    8.26 +apply(induct_tac a and b)
    8.27  
    8.28  txt{*\noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:
    8.29  *}
    8.30  
    8.31 -apply simp_all;
    8.32 +apply simp_all
    8.33  (*<*)done(*>*)
    8.34  
    8.35  text{*
     9.1 --- a/src/Doc/Tutorial/Datatype/Fundata.thy	Sat Nov 01 11:40:55 2014 +0100
     9.2 +++ b/src/Doc/Tutorial/Datatype/Fundata.thy	Sat Nov 01 14:20:38 2014 +0100
     9.3 @@ -34,10 +34,10 @@
     9.4  
     9.5  The following lemma has a simple proof by induction:  *}
     9.6  
     9.7 -lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
     9.8 +lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
     9.9  apply(induct_tac T, simp_all)
    9.10  done
    9.11 -(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
    9.12 +(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"
    9.13  apply(induct_tac T, rename_tac[2] F)(*>*)
    9.14  txt{*\noindent
    9.15  Because of the function type, the proof state after induction looks unusual.
    10.1 --- a/src/Doc/Tutorial/Datatype/Nested.thy	Sat Nov 01 11:40:55 2014 +0100
    10.2 +++ b/src/Doc/Tutorial/Datatype/Nested.thy	Sat Nov 01 14:20:38 2014 +0100
    10.3 @@ -12,7 +12,7 @@
    10.4  where function symbols can be applied to a list of arguments:
    10.5  *}
    10.6  (*<*)hide_const Var(*>*)
    10.7 -datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list";
    10.8 +datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"
    10.9  
   10.10  text{*\noindent
   10.11  Note that we need to quote @{text term} on the left to avoid confusion with
   10.12 @@ -66,8 +66,8 @@
   10.13  *}
   10.14  
   10.15  lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst  Var t  = (t ::('v,'f)term)  \<and>
   10.16 -                  substs Var ts = (ts::('v,'f)term list)";
   10.17 -apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all);
   10.18 +                  substs Var ts = (ts::('v,'f)term list)"
   10.19 +apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all)
   10.20  done
   10.21  
   10.22  text{*\noindent
    11.1 --- a/src/Doc/Tutorial/Datatype/unfoldnested.thy	Sat Nov 01 11:40:55 2014 +0100
    11.2 +++ b/src/Doc/Tutorial/Datatype/unfoldnested.thy	Sat Nov 01 14:20:38 2014 +0100
    11.3 @@ -1,5 +1,5 @@
    11.4  (*<*)
    11.5 -theory unfoldnested imports Main begin;
    11.6 +theory unfoldnested imports Main begin
    11.7  (*>*)
    11.8  datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term_list"
    11.9  and ('v,'f)term_list = Nil | Cons "('v,'f)term" "('v,'f)term_list"
    12.1 --- a/src/Doc/Tutorial/Fun/fun0.thy	Sat Nov 01 11:40:55 2014 +0100
    12.2 +++ b/src/Doc/Tutorial/Fun/fun0.thy	Sat Nov 01 14:20:38 2014 +0100
    12.3 @@ -27,7 +27,7 @@
    12.4  fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    12.5  "sep a []     = []" |
    12.6  "sep a [x]    = [x]" |
    12.7 -"sep a (x#y#zs) = x # a # sep a (y#zs)";
    12.8 +"sep a (x#y#zs) = x # a # sep a (y#zs)"
    12.9  
   12.10  text{*\noindent
   12.11  This time the length of the list decreases with the
   12.12 @@ -217,7 +217,7 @@
   12.13  this lemma by recursion induction over @{term"sep"}:
   12.14  *}
   12.15  
   12.16 -apply(induct_tac x xs rule: sep.induct);
   12.17 +apply(induct_tac x xs rule: sep.induct)
   12.18  
   12.19  txt{*\noindent
   12.20  The resulting proof state has three subgoals corresponding to the three
   12.21 @@ -226,7 +226,7 @@
   12.22  The rest is pure simplification:
   12.23  *}
   12.24  
   12.25 -apply simp_all;
   12.26 +apply simp_all
   12.27  done
   12.28  
   12.29  text{*\noindent The proof goes smoothly because the induction rule
    13.1 --- a/src/Doc/Tutorial/Ifexpr/Ifexpr.thy	Sat Nov 01 11:40:55 2014 +0100
    13.2 +++ b/src/Doc/Tutorial/Ifexpr/Ifexpr.thy	Sat Nov 01 14:20:38 2014 +0100
    13.3 @@ -1,5 +1,5 @@
    13.4  (*<*)
    13.5 -theory Ifexpr imports Main begin;
    13.6 +theory Ifexpr imports Main begin
    13.7  (*>*)
    13.8  
    13.9  subsection{*Case Study: Boolean Expressions*}
   13.10 @@ -19,7 +19,7 @@
   13.11  *}
   13.12  
   13.13  datatype boolex = Const bool | Var nat | Neg boolex
   13.14 -                | And boolex boolex;
   13.15 +                | And boolex boolex
   13.16  
   13.17  text{*\noindent
   13.18  The two constants are represented by @{term"Const True"} and
   13.19 @@ -51,7 +51,7 @@
   13.20  (@{term"IF"}):
   13.21  *}
   13.22  
   13.23 -datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
   13.24 +datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex
   13.25  
   13.26  text{*\noindent
   13.27  The evaluation of If-expressions proceeds as for @{typ"boolex"}:
   13.28 @@ -82,14 +82,14 @@
   13.29  value of its argument:
   13.30  *}
   13.31  
   13.32 -lemma "valif (bool2if b) env = value b env";
   13.33 +lemma "valif (bool2if b) env = value b env"
   13.34  
   13.35  txt{*\noindent
   13.36  The proof is canonical:
   13.37  *}
   13.38  
   13.39 -apply(induct_tac b);
   13.40 -apply(auto);
   13.41 +apply(induct_tac b)
   13.42 +apply(auto)
   13.43  done
   13.44  
   13.45  text{*\noindent
   13.46 @@ -120,7 +120,7 @@
   13.47  transformation preserves the value of the expression:
   13.48  *}
   13.49  
   13.50 -theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
   13.51 +theorem "valif (norm b) env = valif b env"(*<*)oops(*>*)
   13.52  
   13.53  text{*\noindent
   13.54  The proof is canonical, provided we first show the following simplification
   13.55 @@ -128,14 +128,14 @@
   13.56  *}
   13.57  
   13.58  lemma [simp]:
   13.59 -  "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
   13.60 +  "\<forall>t e. valif (normif b t e) env = valif (IF b t e) env"
   13.61  (*<*)
   13.62 -apply(induct_tac b);
   13.63 -by(auto);
   13.64 +apply(induct_tac b)
   13.65 +by(auto)
   13.66  
   13.67 -theorem "valif (norm b) env = valif b env";
   13.68 -apply(induct_tac b);
   13.69 -by(auto);
   13.70 +theorem "valif (norm b) env = valif b env"
   13.71 +apply(induct_tac b)
   13.72 +by(auto)
   13.73  (*>*)
   13.74  text{*\noindent
   13.75  Note that the lemma does not have a name, but is implicitly used in the proof
   13.76 @@ -156,14 +156,14 @@
   13.77  normality of @{term"normif"}:
   13.78  *}
   13.79  
   13.80 -lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)";
   13.81 +lemma [simp]: "\<forall>t e. normal(normif b t e) = (normal t \<and> normal e)"
   13.82  (*<*)
   13.83 -apply(induct_tac b);
   13.84 -by(auto);
   13.85 +apply(induct_tac b)
   13.86 +by(auto)
   13.87  
   13.88 -theorem "normal(norm b)";
   13.89 -apply(induct_tac b);
   13.90 -by(auto);
   13.91 +theorem "normal(norm b)"
   13.92 +apply(induct_tac b)
   13.93 +by(auto)
   13.94  (*>*)
   13.95  
   13.96  text{*\medskip
    14.1 --- a/src/Doc/Tutorial/Inductive/Star.thy	Sat Nov 01 11:40:55 2014 +0100
    14.2 +++ b/src/Doc/Tutorial/Inductive/Star.thy	Sat Nov 01 14:20:38 2014 +0100
    14.3 @@ -39,7 +39,7 @@
    14.4  *}
    14.5  
    14.6  lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
    14.7 -by(blast intro: rtc_step);
    14.8 +by(blast intro: rtc_step)
    14.9  
   14.10  text{*\noindent
   14.11  Although the lemma itself is an unremarkable consequence of the basic rules,
   14.12 @@ -110,8 +110,8 @@
   14.13  @{subgoals[display,indent=0]}
   14.14  *}
   14.15  
   14.16 - apply(blast);
   14.17 -apply(blast intro: rtc_step);
   14.18 + apply(blast)
   14.19 +apply(blast intro: rtc_step)
   14.20  done
   14.21  
   14.22  text{*
   14.23 @@ -134,16 +134,16 @@
   14.24  *}
   14.25  
   14.26  lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
   14.27 -apply(erule rtc2.induct);
   14.28 -  apply(blast);
   14.29 - apply(blast);
   14.30 -apply(blast intro: rtc_trans);
   14.31 +apply(erule rtc2.induct)
   14.32 +  apply(blast)
   14.33 + apply(blast)
   14.34 +apply(blast intro: rtc_trans)
   14.35  done
   14.36  
   14.37  lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
   14.38 -apply(erule rtc.induct);
   14.39 - apply(blast intro: rtc2.intros);
   14.40 -apply(blast intro: rtc2.intros);
   14.41 +apply(erule rtc.induct)
   14.42 + apply(blast intro: rtc2.intros)
   14.43 +apply(blast intro: rtc2.intros)
   14.44  done
   14.45  
   14.46  text{*
   14.47 @@ -167,8 +167,8 @@
   14.48  *}
   14.49  (*<*)
   14.50  lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
   14.51 -apply(erule rtc.induct);
   14.52 - apply blast;
   14.53 +apply(erule rtc.induct)
   14.54 + apply blast
   14.55  apply(blast intro: rtc_step)
   14.56  done
   14.57  
    15.1 --- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat Nov 01 11:40:55 2014 +0100
    15.2 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat Nov 01 14:20:38 2014 +0100
    15.3 @@ -1,5 +1,5 @@
    15.4  (*<*)
    15.5 -theory AdvancedInd imports Main begin;
    15.6 +theory AdvancedInd imports Main begin
    15.7  (*>*)
    15.8  
    15.9  text{*\noindent
   15.10 @@ -9,9 +9,9 @@
   15.11  (\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
   15.12  and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
   15.13  with an extended example of induction (\S\ref{sec:CTL-revisited}).
   15.14 -*};
   15.15 +*}
   15.16  
   15.17 -subsection{*Massaging the Proposition*};
   15.18 +subsection{*Massaging the Proposition*}
   15.19  
   15.20  text{*\label{sec:ind-var-in-prems}
   15.21  Often we have assumed that the theorem to be proved is already in a form
   15.22 @@ -19,7 +19,7 @@
   15.23  Here is an example.
   15.24  Since @{term"hd"} and @{term"last"} return the first and last element of a
   15.25  non-empty list, this lemma looks easy to prove:
   15.26 -*};
   15.27 +*}
   15.28  
   15.29  lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
   15.30  apply(induct_tac xs)
   15.31 @@ -51,11 +51,11 @@
   15.32  implication~(@{text"\<longrightarrow>"}), letting
   15.33  \attrdx{rule_format} (\S\ref{sec:forward}) convert the
   15.34  result to the usual @{text"\<Longrightarrow>"} form:
   15.35 -*};
   15.36 -(*<*)oops;(*>*)
   15.37 -lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
   15.38 +*}
   15.39 +(*<*)oops(*>*)
   15.40 +lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"
   15.41  (*<*)
   15.42 -apply(induct_tac xs);
   15.43 +apply(induct_tac xs)
   15.44  (*>*)
   15.45  
   15.46  txt{*\noindent
   15.47 @@ -112,7 +112,7 @@
   15.48  *}
   15.49  (*<*)by auto(*>*)
   15.50  
   15.51 -subsection{*Beyond Structural and Recursion Induction*};
   15.52 +subsection{*Beyond Structural and Recursion Induction*}
   15.53  
   15.54  text{*\label{sec:complete-ind}
   15.55  So far, inductive proofs were by structural induction for
   15.56 @@ -130,7 +130,7 @@
   15.57  @{thm[display]"nat_less_induct"[no_vars]}
   15.58  As an application, we prove a property of the following
   15.59  function:
   15.60 -*};
   15.61 +*}
   15.62  
   15.63  axiomatization f :: "nat \<Rightarrow> nat"
   15.64    where f_ax: "f(f(n)) < f(Suc(n))"
   15.65 @@ -148,17 +148,17 @@
   15.66  The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
   15.67  be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
   15.68  above, we have to phrase the proposition as follows to allow induction:
   15.69 -*};
   15.70 +*}
   15.71  
   15.72 -lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
   15.73 +lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
   15.74  
   15.75  txt{*\noindent
   15.76  To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
   15.77  the same general induction method as for recursion induction (see
   15.78  \S\ref{sec:fun-induction}):
   15.79 -*};
   15.80 +*}
   15.81  
   15.82 -apply(induct_tac k rule: nat_less_induct);
   15.83 +apply(induct_tac k rule: nat_less_induct)
   15.84  
   15.85  txt{*\noindent
   15.86  We get the following proof state:
   15.87 @@ -203,17 +203,17 @@
   15.88  proofs are easy to write but hard to read and understand.
   15.89  
   15.90  The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
   15.91 -*};
   15.92 +*}
   15.93  
   15.94 -lemmas f_incr = f_incr_lem[rule_format, OF refl];
   15.95 +lemmas f_incr = f_incr_lem[rule_format, OF refl]
   15.96  
   15.97  text{*\noindent
   15.98  The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. 
   15.99  We could have included this derivation in the original statement of the lemma:
  15.100 -*};
  15.101 +*}
  15.102  
  15.103 -lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
  15.104 -(*<*)oops;(*>*)
  15.105 +lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
  15.106 +(*<*)oops(*>*)
  15.107  
  15.108  text{*
  15.109  \begin{exercise}
  15.110 @@ -237,7 +237,7 @@
  15.111  where @{term f} may be any function into type @{typ nat}.
  15.112  *}
  15.113  
  15.114 -subsection{*Derivation of New Induction Schemas*};
  15.115 +subsection{*Derivation of New Induction Schemas*}
  15.116  
  15.117  text{*\label{sec:derive-ind}
  15.118  \index{induction!deriving new schemas}%
  15.119 @@ -246,18 +246,18 @@
  15.120  of @{thm[source]nat_less_induct}. Assume we only have structural induction
  15.121  available for @{typ"nat"} and want to derive complete induction.  We
  15.122  must generalize the statement as shown:
  15.123 -*};
  15.124 +*}
  15.125  
  15.126 -lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
  15.127 -apply(induct_tac n);
  15.128 +lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m"
  15.129 +apply(induct_tac n)
  15.130  
  15.131  txt{*\noindent
  15.132  The base case is vacuously true. For the induction step (@{prop"m <
  15.133  Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
  15.134  hypothesis and case @{prop"m = n"} follows from the assumption, again using
  15.135  the induction hypothesis:
  15.136 -*};
  15.137 - apply(blast);
  15.138 +*}
  15.139 + apply(blast)
  15.140  by(blast elim: less_SucE)
  15.141  
  15.142  text{*\noindent
  15.143 @@ -270,10 +270,10 @@
  15.144  and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
  15.145  happens automatically when we add the lemma as a new premise to the
  15.146  desired goal:
  15.147 -*};
  15.148 +*}
  15.149  
  15.150 -theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
  15.151 -by(insert induct_lem, blast);
  15.152 +theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"
  15.153 +by(insert induct_lem, blast)
  15.154  
  15.155  text{*
  15.156  HOL already provides the mother of
    16.1 --- a/src/Doc/Tutorial/Misc/Itrev.thy	Sat Nov 01 11:40:55 2014 +0100
    16.2 +++ b/src/Doc/Tutorial/Misc/Itrev.thy	Sat Nov 01 14:20:38 2014 +0100
    16.3 @@ -58,15 +58,15 @@
    16.4  
    16.5  Naturally, we would like to show that @{term"itrev"} does indeed reverse
    16.6  its first argument provided the second one is empty:
    16.7 -*};
    16.8 +*}
    16.9  
   16.10 -lemma "itrev xs [] = rev xs";
   16.11 +lemma "itrev xs [] = rev xs"
   16.12  
   16.13  txt{*\noindent
   16.14  There is no choice as to the induction variable, and we immediately simplify:
   16.15 -*};
   16.16 +*}
   16.17  
   16.18 -apply(induct_tac xs, simp_all);
   16.19 +apply(induct_tac xs, simp_all)
   16.20  
   16.21  txt{*\noindent
   16.22  Unfortunately, this attempt does not prove
   16.23 @@ -80,9 +80,9 @@
   16.24  \end{quote}
   16.25  Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
   16.26  just not true.  The correct generalization is
   16.27 -*};
   16.28 -(*<*)oops;(*>*)
   16.29 -lemma "itrev xs ys = rev xs @ ys";
   16.30 +*}
   16.31 +(*<*)oops(*>*)
   16.32 +lemma "itrev xs ys = rev xs @ ys"
   16.33  (*<*)apply(induct_tac xs, simp_all)(*>*)
   16.34  txt{*\noindent
   16.35  If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
   16.36 @@ -100,11 +100,11 @@
   16.37  the subgoal, but the induction hypothesis needs to be applied with
   16.38  @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
   16.39  for all @{term"ys"} instead of a fixed one:
   16.40 -*};
   16.41 -(*<*)oops;(*>*)
   16.42 -lemma "\<forall>ys. itrev xs ys = rev xs @ ys";
   16.43 +*}
   16.44 +(*<*)oops(*>*)
   16.45 +lemma "\<forall>ys. itrev xs ys = rev xs @ ys"
   16.46  (*<*)
   16.47 -by(induct_tac xs, simp_all);
   16.48 +by(induct_tac xs, simp_all)
   16.49  (*>*)
   16.50  
   16.51  text{*\noindent
    17.1 --- a/src/Doc/Tutorial/Misc/Option2.thy	Sat Nov 01 11:40:55 2014 +0100
    17.2 +++ b/src/Doc/Tutorial/Misc/Option2.thy	Sat Nov 01 14:20:38 2014 +0100
    17.3 @@ -9,7 +9,7 @@
    17.4  Our final datatype is very simple but still eminently useful:
    17.5  *}
    17.6  
    17.7 -datatype 'a option = None | Some 'a;
    17.8 +datatype 'a option = None | Some 'a
    17.9  
   17.10  text{*\noindent
   17.11  Frequently one needs to add a distinguished element to some existing type.
    18.1 --- a/src/Doc/Tutorial/Misc/Tree.thy	Sat Nov 01 11:40:55 2014 +0100
    18.2 +++ b/src/Doc/Tutorial/Misc/Tree.thy	Sat Nov 01 14:20:38 2014 +0100
    18.3 @@ -6,25 +6,25 @@
    18.4  Define the datatype of \rmindex{binary trees}:
    18.5  *}
    18.6  
    18.7 -datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
    18.8 +datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
    18.9  
   18.10  primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   18.11  "mirror Tip = Tip" |
   18.12 -"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
   18.13 +"mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
   18.14  
   18.15  text{*\noindent
   18.16  Define a function @{term"mirror"} that mirrors a binary tree
   18.17  by swapping subtrees recursively. Prove
   18.18  *}
   18.19  
   18.20 -lemma mirror_mirror: "mirror(mirror t) = t";
   18.21 +lemma mirror_mirror: "mirror(mirror t) = t"
   18.22  (*<*)
   18.23 -apply(induct_tac t);
   18.24 -by(auto);
   18.25 +apply(induct_tac t)
   18.26 +by(auto)
   18.27  
   18.28  primrec flatten :: "'a tree => 'a list" where
   18.29  "flatten Tip = []" |
   18.30 -"flatten (Node l x r) = flatten l @ [x] @ flatten r";
   18.31 +"flatten (Node l x r) = flatten l @ [x] @ flatten r"
   18.32  (*>*)
   18.33  
   18.34  text{*\noindent
   18.35 @@ -32,10 +32,10 @@
   18.36  by traversing it in infix order. Prove
   18.37  *}
   18.38  
   18.39 -lemma "flatten(mirror t) = rev(flatten t)";
   18.40 +lemma "flatten(mirror t) = rev(flatten t)"
   18.41  (*<*)
   18.42 -apply(induct_tac t);
   18.43 -by(auto);
   18.44 +apply(induct_tac t)
   18.45 +by(auto)
   18.46  
   18.47  end
   18.48  (*>*)
    19.1 --- a/src/Doc/Tutorial/Misc/Tree2.thy	Sat Nov 01 11:40:55 2014 +0100
    19.2 +++ b/src/Doc/Tutorial/Misc/Tree2.thy	Sat Nov 01 14:20:38 2014 +0100
    19.3 @@ -16,7 +16,7 @@
    19.4  (*<*)
    19.5  lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs"
    19.6  apply(induct_tac t)
    19.7 -by(auto);
    19.8 +by(auto)
    19.9  (*>*)
   19.10  lemma "flatten2 t [] = flatten t"
   19.11  (*<*)
    20.1 --- a/src/Doc/Tutorial/Misc/case_exprs.thy	Sat Nov 01 11:40:55 2014 +0100
    20.2 +++ b/src/Doc/Tutorial/Misc/case_exprs.thy	Sat Nov 01 14:20:38 2014 +0100
    20.3 @@ -52,8 +52,8 @@
    20.4  by \methdx{case_tac}.  Here is a trivial example:
    20.5  *}
    20.6  
    20.7 -lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
    20.8 -apply(case_tac xs);
    20.9 +lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"
   20.10 +apply(case_tac xs)
   20.11  
   20.12  txt{*\noindent
   20.13  results in the proof state
    21.1 --- a/src/Doc/Tutorial/Misc/fakenat.thy	Sat Nov 01 11:40:55 2014 +0100
    21.2 +++ b/src/Doc/Tutorial/Misc/fakenat.thy	Sat Nov 01 14:20:38 2014 +0100
    21.3 @@ -1,5 +1,5 @@
    21.4  (*<*)
    21.5 -theory fakenat imports Main begin;
    21.6 +theory fakenat imports Main begin
    21.7  (*>*)
    21.8  
    21.9  text{*\noindent
    22.1 --- a/src/Doc/Tutorial/Misc/pairs2.thy	Sat Nov 01 11:40:55 2014 +0100
    22.2 +++ b/src/Doc/Tutorial/Misc/pairs2.thy	Sat Nov 01 14:20:38 2014 +0100
    22.3 @@ -1,5 +1,5 @@
    22.4  (*<*)
    22.5 -theory pairs2 imports Main begin;
    22.6 +theory pairs2 imports Main begin
    22.7  (*>*)
    22.8  text{*\label{sec:pairs}\index{pairs and tuples}
    22.9  HOL also has ordered pairs: \isa{($a@1$,$a@2$)} is of type $\tau@1$
    23.1 --- a/src/Doc/Tutorial/Misc/prime_def.thy	Sat Nov 01 11:40:55 2014 +0100
    23.2 +++ b/src/Doc/Tutorial/Misc/prime_def.thy	Sat Nov 01 14:20:38 2014 +0100
    23.3 @@ -1,5 +1,5 @@
    23.4  (*<*)
    23.5 -theory prime_def imports Main begin;
    23.6 +theory prime_def imports Main begin
    23.7  consts prime :: "nat \<Rightarrow> bool"
    23.8  (*>*)
    23.9  text{*
    24.1 --- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Nov 01 11:40:55 2014 +0100
    24.2 +++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Nov 01 14:20:38 2014 +0100
    24.3 @@ -278,7 +278,7 @@
    24.4  text{*For proving @{text new_keys_not_used}*}
    24.5  lemma keysFor_parts_insert:
    24.6       "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
    24.7 -      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
    24.8 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H" 
    24.9  by (force 
   24.10      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   24.11             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
    25.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Sat Nov 01 11:40:55 2014 +0100
    25.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Sat Nov 01 14:20:38 2014 +0100
    25.3 @@ -743,7 +743,7 @@
    25.4  
    25.5  lemma Fake_parts_insert_in_Un:
    25.6       "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
    25.7 -      ==> Z \<in>  synth (analz H) \<union> parts H";
    25.8 +      ==> Z \<in>  synth (analz H) \<union> parts H"
    25.9  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
   25.10  
   25.11  text{*@{term H} is sometimes @{term"Key ` KK \<union> spies evs"}, so can't put 
   25.12 @@ -882,24 +882,24 @@
   25.13  apply (drule synth_mono)
   25.14  apply (simp add: synth_idem)
   25.15  apply (rule equalityI)
   25.16 -apply (simp add: );
   25.17 +apply (simp add: )
   25.18  apply (rule synth_analz_mono, blast)   
   25.19  done
   25.20  
   25.21  text{*Two generalizations of @{text analz_insert_eq}*}
   25.22  lemma gen_analz_insert_eq [rule_format]:
   25.23 -     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   25.24 +     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
   25.25  by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   25.26  
   25.27  lemma synth_analz_insert_eq [rule_format]:
   25.28       "X \<in> synth (analz H) 
   25.29 -      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   25.30 +      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
   25.31  apply (erule synth.induct) 
   25.32  apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) 
   25.33  done
   25.34  
   25.35  lemma Fake_parts_sing:
   25.36 -     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   25.37 +     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
   25.38  apply (rule subset_trans) 
   25.39   apply (erule_tac [2] Fake_parts_insert)
   25.40  apply (rule parts_mono, blast)
    26.1 --- a/src/Doc/Tutorial/Recdef/Induction.thy	Sat Nov 01 11:40:55 2014 +0100
    26.2 +++ b/src/Doc/Tutorial/Recdef/Induction.thy	Sat Nov 01 14:20:38 2014 +0100
    26.3 @@ -1,5 +1,5 @@
    26.4  (*<*)
    26.5 -theory Induction imports examples simplification begin;
    26.6 +theory Induction imports examples simplification begin
    26.7  (*>*)
    26.8  
    26.9  text{*
   26.10 @@ -19,7 +19,7 @@
   26.11  involving the predefined @{term"map"} functional on lists:
   26.12  *}
   26.13  
   26.14 -lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
   26.15 +lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
   26.16  
   26.17  txt{*\noindent
   26.18  Note that @{term"map f xs"}
   26.19 @@ -27,7 +27,7 @@
   26.20  this lemma by recursion induction over @{term"sep"}:
   26.21  *}
   26.22  
   26.23 -apply(induct_tac x xs rule: sep.induct);
   26.24 +apply(induct_tac x xs rule: sep.induct)
   26.25  
   26.26  txt{*\noindent
   26.27  The resulting proof state has three subgoals corresponding to the three
   26.28 @@ -36,7 +36,7 @@
   26.29  The rest is pure simplification:
   26.30  *}
   26.31  
   26.32 -apply simp_all;
   26.33 +apply simp_all
   26.34  done
   26.35  
   26.36  text{*
    27.1 --- a/src/Doc/Tutorial/Recdef/examples.thy	Sat Nov 01 11:40:55 2014 +0100
    27.2 +++ b/src/Doc/Tutorial/Recdef/examples.thy	Sat Nov 01 14:20:38 2014 +0100
    27.3 @@ -1,16 +1,16 @@
    27.4  (*<*)
    27.5 -theory examples imports Main begin;
    27.6 +theory examples imports Main begin
    27.7  (*>*)
    27.8  
    27.9  text{*
   27.10  Here is a simple example, the \rmindex{Fibonacci function}:
   27.11  *}
   27.12  
   27.13 -consts fib :: "nat \<Rightarrow> nat";
   27.14 +consts fib :: "nat \<Rightarrow> nat"
   27.15  recdef fib "measure(\<lambda>n. n)"
   27.16    "fib 0 = 0"
   27.17    "fib (Suc 0) = 1"
   27.18 -  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
   27.19 +  "fib (Suc(Suc x)) = fib x + fib (Suc x)"
   27.20  
   27.21  text{*\noindent
   27.22  \index{measure functions}%
   27.23 @@ -27,11 +27,11 @@
   27.24  between any two elements of a list:
   27.25  *}
   27.26  
   27.27 -consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list";
   27.28 +consts sep :: "'a \<times> 'a list \<Rightarrow> 'a list"
   27.29  recdef sep "measure (\<lambda>(a,xs). length xs)"
   27.30    "sep(a, [])     = []"
   27.31    "sep(a, [x])    = [x]"
   27.32 -  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
   27.33 +  "sep(a, x#y#zs) = x # a # sep(a,y#zs)"
   27.34  
   27.35  text{*\noindent
   27.36  This time the measure is the length of the list, which decreases with the
   27.37 @@ -43,20 +43,20 @@
   27.38  need not be exhaustive:
   27.39  *}
   27.40  
   27.41 -consts last :: "'a list \<Rightarrow> 'a";
   27.42 +consts last :: "'a list \<Rightarrow> 'a"
   27.43  recdef last "measure (\<lambda>xs. length xs)"
   27.44    "last [x]      = x"
   27.45 -  "last (x#y#zs) = last (y#zs)";
   27.46 +  "last (x#y#zs) = last (y#zs)"
   27.47  
   27.48  text{*
   27.49  Overlapping patterns are disambiguated by taking the order of equations into
   27.50  account, just as in functional programming:
   27.51  *}
   27.52  
   27.53 -consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list";
   27.54 +consts sep1 :: "'a \<times> 'a list \<Rightarrow> 'a list"
   27.55  recdef sep1 "measure (\<lambda>(a,xs). length xs)"
   27.56    "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
   27.57 -  "sep1(a, xs)     = xs";
   27.58 +  "sep1(a, xs)     = xs"
   27.59  
   27.60  text{*\noindent
   27.61  To guarantee that the second equation can only be applied if the first
   27.62 @@ -74,10 +74,10 @@
   27.63    arguments as in the following definition:
   27.64  \end{warn}
   27.65  *}
   27.66 -consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list";
   27.67 +consts sep2 :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list"
   27.68  recdef sep2 "measure length"
   27.69    "sep2 (x#y#zs) = (\<lambda>a. x # a # sep2 (y#zs) a)"
   27.70 -  "sep2 xs       = (\<lambda>a. xs)";
   27.71 +  "sep2 xs       = (\<lambda>a. xs)"
   27.72  
   27.73  text{*
   27.74  Because of its pattern-matching syntax, \isacommand{recdef} is also useful
   27.75 @@ -85,10 +85,10 @@
   27.76  degenerates to the empty set @{term"{}"}:
   27.77  *}
   27.78  
   27.79 -consts swap12 :: "'a list \<Rightarrow> 'a list";
   27.80 +consts swap12 :: "'a list \<Rightarrow> 'a list"
   27.81  recdef swap12 "{}"
   27.82    "swap12 (x#y#zs) = y#x#zs"
   27.83 -  "swap12 zs       = zs";
   27.84 +  "swap12 zs       = zs"
   27.85  
   27.86  (*<*)
   27.87  end
    28.1 --- a/src/Doc/Tutorial/Recdef/simplification.thy	Sat Nov 01 11:40:55 2014 +0100
    28.2 +++ b/src/Doc/Tutorial/Recdef/simplification.thy	Sat Nov 01 14:20:38 2014 +0100
    28.3 @@ -1,5 +1,5 @@
    28.4  (*<*)
    28.5 -theory simplification imports Main begin;
    28.6 +theory simplification imports Main begin
    28.7  (*>*)
    28.8  
    28.9  text{*
   28.10 @@ -12,9 +12,9 @@
   28.11  Let us look at an example:
   28.12  *}
   28.13  
   28.14 -consts gcd :: "nat\<times>nat \<Rightarrow> nat";
   28.15 +consts gcd :: "nat\<times>nat \<Rightarrow> nat"
   28.16  recdef gcd "measure (\<lambda>(m,n).n)"
   28.17 -  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
   28.18 +  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
   28.19  
   28.20  text{*\noindent
   28.21  According to the measure function, the second argument should decrease with
   28.22 @@ -50,10 +50,10 @@
   28.23  following alternative definition suggests itself:
   28.24  *}
   28.25  
   28.26 -consts gcd1 :: "nat\<times>nat \<Rightarrow> nat";
   28.27 +consts gcd1 :: "nat\<times>nat \<Rightarrow> nat"
   28.28  recdef gcd1 "measure (\<lambda>(m,n).n)"
   28.29    "gcd1 (m, 0) = m"
   28.30 -  "gcd1 (m, n) = gcd1(n, m mod n)";
   28.31 +  "gcd1 (m, n) = gcd1(n, m mod n)"
   28.32  
   28.33  
   28.34  text{*\noindent
   28.35 @@ -65,9 +65,9 @@
   28.36  which is also available for @{typ bool} and is not split automatically:
   28.37  *}
   28.38  
   28.39 -consts gcd2 :: "nat\<times>nat \<Rightarrow> nat";
   28.40 +consts gcd2 :: "nat\<times>nat \<Rightarrow> nat"
   28.41  recdef gcd2 "measure (\<lambda>(m,n).n)"
   28.42 -  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))";
   28.43 +  "gcd2(m,n) = (case n=0 of True \<Rightarrow> m | False \<Rightarrow> gcd2(n,m mod n))"
   28.44  
   28.45  text{*\noindent
   28.46  This is probably the neatest solution next to pattern matching, and it is
   28.47 @@ -78,12 +78,12 @@
   28.48  these lemmas:
   28.49  *}
   28.50  
   28.51 -lemma [simp]: "gcd (m, 0) = m";
   28.52 -apply(simp);
   28.53 +lemma [simp]: "gcd (m, 0) = m"
   28.54 +apply(simp)
   28.55  done
   28.56  
   28.57 -lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
   28.58 -apply(simp);
   28.59 +lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m, n) = gcd(n, m mod n)"
   28.60 +apply(simp)
   28.61  done
   28.62  
   28.63  text{*\noindent
    29.1 --- a/src/Doc/Tutorial/Rules/Blast.thy	Sat Nov 01 11:40:55 2014 +0100
    29.2 +++ b/src/Doc/Tutorial/Rules/Blast.thy	Sat Nov 01 14:20:38 2014 +0100
    29.3 @@ -13,7 +13,7 @@
    29.4         (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and> 
    29.5         (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and> 
    29.6         (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))  
    29.7 -       \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
    29.8 +       \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"
    29.9  by blast
   29.10  
   29.11  lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
   29.12 @@ -26,12 +26,12 @@
   29.13  
   29.14  @{thm[display] finite_Un}
   29.15   \rulename{finite_Un}}
   29.16 -*};
   29.17 +*}
   29.18  
   29.19  
   29.20  lemma [iff]: "(xs@ys = []) = (xs=[] & ys=[])"
   29.21    apply (induct_tac xs)
   29.22 -  by (simp_all);
   29.23 +  by (simp_all)
   29.24  
   29.25  (*ideas for uses of intro, etc.: ex/Primes/is_gcd_unique?*)
   29.26  end
    30.1 --- a/src/Doc/Tutorial/Rules/Force.thy	Sat Nov 01 11:40:55 2014 +0100
    30.2 +++ b/src/Doc/Tutorial/Rules/Force.thy	Sat Nov 01 14:20:38 2014 +0100
    30.3 @@ -2,7 +2,7 @@
    30.4    (*Use Divides rather than Main to experiment with the first proof.
    30.5      Otherwise, it is done by the nat_divide_cancel_factor simprocs.*)
    30.6  
    30.7 -declare div_mult_self_is_m [simp del];
    30.8 +declare div_mult_self_is_m [simp del]
    30.9  
   30.10  lemma div_mult_self_is_m: 
   30.11        "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
   30.12 @@ -21,14 +21,14 @@
   30.13  goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
   30.14  {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ Q\ x{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x\ {\isasymand}\ Q\ x{\isacharparenright}\isanewline
   30.15  \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ xa{\isachardot}\ {\isasymlbrakk}{\isasymforall}x{\isachardot}\ P\ x{\isacharsemicolon}\ Q\ xa{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x\ {\isasymand}\ Q\ x
   30.16 -*};
   30.17 +*}
   30.18  
   30.19  text {*
   30.20  couldn't find a good example of clarsimp
   30.21  
   30.22  @{thm[display]"someI"}
   30.23  \rulename{someI}
   30.24 -*};
   30.25 +*}
   30.26  
   30.27  lemma "\<lbrakk>Q a; P a\<rbrakk> \<Longrightarrow> P (SOME x. P x \<and> Q x) \<and> Q (SOME x. P x \<and> Q x)"
   30.28  apply (rule someI)
    31.1 --- a/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 11:40:55 2014 +0100
    31.2 +++ b/src/Doc/Tutorial/Rules/Forward.thy	Sat Nov 01 14:20:38 2014 +0100
    31.3 @@ -11,7 +11,7 @@
    31.4  (** Commutativity **)
    31.5  
    31.6  lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
    31.7 -apply (auto simp add: is_gcd_def);
    31.8 +apply (auto simp add: is_gcd_def)
    31.9  done
   31.10  
   31.11  lemma gcd_commute: "gcd m n = gcd n m"
   31.12 @@ -48,15 +48,15 @@
   31.13  text {*
   31.14  @{thm[display] gcd_mult_distrib2}
   31.15  \rulename{gcd_mult_distrib2}
   31.16 -*};
   31.17 +*}
   31.18  
   31.19  text{*\noindent
   31.20  of, simplified
   31.21  *}
   31.22  
   31.23  
   31.24 -lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1];
   31.25 -lemmas gcd_mult_1 = gcd_mult_0 [simplified];
   31.26 +lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
   31.27 +lemmas gcd_mult_1 = gcd_mult_0 [simplified]
   31.28  
   31.29  lemmas where1 = gcd_mult_distrib2 [where m=1]
   31.30  
   31.31 @@ -82,23 +82,23 @@
   31.32  
   31.33  @{thm[display] sym}
   31.34  \rulename{sym}
   31.35 -*};
   31.36 +*}
   31.37  
   31.38 -lemmas gcd_mult0 = gcd_mult_1 [THEN sym];
   31.39 +lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
   31.40        (*not quite right: we need ?k but this gives k*)
   31.41  
   31.42 -lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym];
   31.43 +lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
   31.44        (*better in one step!*)
   31.45  
   31.46  text {*
   31.47  more legible, and variables properly generalized
   31.48 -*};
   31.49 +*}
   31.50  
   31.51  lemma gcd_mult [simp]: "gcd k (k*n) = k"
   31.52  by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
   31.53  
   31.54  
   31.55 -lemmas gcd_self0 = gcd_mult [of k 1, simplified];
   31.56 +lemmas gcd_self0 = gcd_mult [of k 1, simplified]
   31.57  
   31.58  
   31.59  text {*
   31.60 @@ -107,7 +107,7 @@
   31.61  
   31.62  @{thm[display] gcd_self0}
   31.63  \rulename{gcd_self0}
   31.64 -*};
   31.65 +*}
   31.66  
   31.67  text {*
   31.68  Rules handy with THEN
   31.69 @@ -117,12 +117,12 @@
   31.70  
   31.71  @{thm[display] iffD2}
   31.72  \rulename{iffD2}
   31.73 -*};
   31.74 +*}
   31.75  
   31.76  
   31.77  text {*
   31.78  again: more legible, and variables properly generalized
   31.79 -*};
   31.80 +*}
   31.81  
   31.82  lemma gcd_self [simp]: "gcd k k = k"
   31.83  by (rule gcd_mult [of k 1, simplified])
   31.84 @@ -143,12 +143,12 @@
   31.85  txt{*
   31.86  before using arg_cong
   31.87  @{subgoals[display,indent=0,margin=65]}
   31.88 -*};
   31.89 +*}
   31.90  apply (drule_tac f="\<lambda>x. x mod u" in arg_cong)
   31.91  txt{*
   31.92  after using arg_cong
   31.93  @{subgoals[display,indent=0,margin=65]}
   31.94 -*};
   31.95 +*}
   31.96  apply (simp add: mod_Suc)
   31.97  done
   31.98  
   31.99 @@ -172,7 +172,7 @@
  31.100  txt{*@{subgoals[display,indent=0,margin=65]}*}
  31.101  apply simp
  31.102  txt{*@{subgoals[display,indent=0,margin=65]}*}
  31.103 -apply (erule_tac t="m" in ssubst);
  31.104 +apply (erule_tac t="m" in ssubst)
  31.105  apply simp
  31.106  done
  31.107  
  31.108 @@ -185,16 +185,16 @@
  31.109  
  31.110  @{thm[display] mod_div_equality}
  31.111  \rulename{mod_div_equality}
  31.112 -*};
  31.113 +*}
  31.114  
  31.115  (*MOVED to Force.thy, which now depends only on Divides.thy
  31.116  lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
  31.117  *)
  31.118  
  31.119 -lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
  31.120 +lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"
  31.121  by (auto intro: relprime_dvd_mult elim: dvdE)
  31.122  
  31.123 -lemma relprime_20_81: "gcd 20 81 = 1";
  31.124 +lemma relprime_20_81: "gcd 20 81 = 1"
  31.125  by (simp add: gcd.simps)
  31.126  
  31.127  text {*
  31.128 @@ -214,20 +214,20 @@
  31.129  @{thm[display] dvd_add [OF dvd_refl dvd_refl]}
  31.130  
  31.131  @{thm[display] dvd_add [OF _ dvd_refl]}
  31.132 -*};
  31.133 +*}
  31.134  
  31.135 -lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)";
  31.136 +lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)"
  31.137  apply (subgoal_tac "z = 34 \<or> z = 36")
  31.138  txt{*
  31.139  the tactic leaves two subgoals:
  31.140  @{subgoals[display,indent=0,margin=65]}
  31.141 -*};
  31.142 +*}
  31.143  apply blast
  31.144  apply (subgoal_tac "z \<noteq> 35")
  31.145  txt{*
  31.146  the tactic leaves two subgoals:
  31.147  @{subgoals[display,indent=0,margin=65]}
  31.148 -*};
  31.149 +*}
  31.150  apply arith
  31.151  apply force
  31.152  done
    32.1 --- a/src/Doc/Tutorial/Rules/TPrimes.thy	Sat Nov 01 11:40:55 2014 +0100
    32.2 +++ b/src/Doc/Tutorial/Rules/TPrimes.thy	Sat Nov 01 14:20:38 2014 +0100
    32.3 @@ -11,20 +11,20 @@
    32.4  text {*Now in Basic.thy!
    32.5  @{thm[display]"dvd_def"}
    32.6  \rulename{dvd_def}
    32.7 -*};
    32.8 +*}
    32.9  
   32.10  
   32.11  (*** Euclid's Algorithm ***)
   32.12  
   32.13  lemma gcd_0 [simp]: "gcd m 0 = m"
   32.14 -apply (simp);
   32.15 +apply (simp)
   32.16  done
   32.17  
   32.18  lemma gcd_non_0 [simp]: "0<n \<Longrightarrow> gcd m n = gcd n (m mod n)"
   32.19  apply (simp)
   32.20 -done;
   32.21 +done
   32.22  
   32.23 -declare gcd.simps [simp del];
   32.24 +declare gcd.simps [simp del]
   32.25  
   32.26  (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
   32.27  lemma gcd_dvd_both: "(gcd m n dvd m) \<and> (gcd m n dvd n)"
   32.28 @@ -33,7 +33,7 @@
   32.29  apply (case_tac "n=0")
   32.30  txt{*subgoals after the case tac
   32.31  @{subgoals[display,indent=0,margin=65]}
   32.32 -*};
   32.33 +*}
   32.34  apply (simp_all) 
   32.35    --{* @{subgoals[display,indent=0,margin=65]} *}
   32.36  by (blast dest: dvd_mod_imp_dvd)
   32.37 @@ -49,7 +49,7 @@
   32.38  *}
   32.39  
   32.40  lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
   32.41 -lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
   32.42 +lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]
   32.43  
   32.44  
   32.45  text {*
   32.46 @@ -60,7 +60,7 @@
   32.47  @{thm[display] gcd_dvd2}
   32.48  \rulename{gcd_dvd2}
   32.49  \end{quote}
   32.50 -*};
   32.51 +*}
   32.52  
   32.53  (*Maximality: for all m,n,k naturals, 
   32.54                  if k divides m and k divides n then k divides gcd(m,n)*)
   32.55 @@ -70,7 +70,7 @@
   32.56  apply (case_tac "n=0")
   32.57  txt{*subgoals after the case tac
   32.58  @{subgoals[display,indent=0,margin=65]}
   32.59 -*};
   32.60 +*}
   32.61  apply (simp_all add: dvd_mod)
   32.62  done
   32.63  
   32.64 @@ -100,12 +100,12 @@
   32.65  
   32.66  (*Function gcd yields the Greatest Common Divisor*)
   32.67  lemma is_gcd: "is_gcd (gcd m n) m n"
   32.68 -apply (simp add: is_gcd_def gcd_greatest);
   32.69 +apply (simp add: is_gcd_def gcd_greatest)
   32.70  done
   32.71  
   32.72  (*uniqueness of GCDs*)
   32.73  lemma is_gcd_unique: "\<lbrakk> is_gcd m a b; is_gcd n a b \<rbrakk> \<Longrightarrow> m=n"
   32.74 -apply (simp add: is_gcd_def);
   32.75 +apply (simp add: is_gcd_def)
   32.76  apply (blast intro: dvd_antisym)
   32.77  done
   32.78  
   32.79 @@ -123,13 +123,13 @@
   32.80  \ \ \ \ \ \ \ n\ dvd\ a\ \isasymand \ n\ dvd\ b\ \isasymand \ (\isasymforall d.\ d\ dvd\ a\ \isasymand \ d\ dvd\ b\ \isasymlongrightarrow \ d\ dvd\ n)\isasymrbrakk \isanewline
   32.81  \ \ \ \ \isasymLongrightarrow \ m\ =\ n
   32.82  \end{isabelle}
   32.83 -*};
   32.84 +*}
   32.85  
   32.86  lemma gcd_assoc: "gcd (gcd k m) n = gcd k (gcd m n)"
   32.87    apply (rule is_gcd_unique)
   32.88    apply (rule is_gcd)
   32.89 -  apply (simp add: is_gcd_def);
   32.90 -  apply (blast intro: dvd_trans);
   32.91 +  apply (simp add: is_gcd_def)
   32.92 +  apply (blast intro: dvd_trans)
   32.93    done
   32.94  
   32.95  text{*
    33.1 --- a/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 11:40:55 2014 +0100
    33.2 +++ b/src/Doc/Tutorial/Sets/Functions.thy	Sat Nov 01 14:20:38 2014 +0100
    33.3 @@ -73,7 +73,7 @@
    33.4  \rulename{fun_eq_iff}
    33.5  *}
    33.6  
    33.7 -lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
    33.8 +lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"
    33.9    apply (simp add: fun_eq_iff inj_on_def)
   33.10    apply (auto)
   33.11    done
    34.1 --- a/src/Doc/Tutorial/Sets/Relations.thy	Sat Nov 01 11:40:55 2014 +0100
    34.2 +++ b/src/Doc/Tutorial/Sets/Relations.thy	Sat Nov 01 14:20:38 2014 +0100
    34.3 @@ -91,7 +91,7 @@
    34.4  apply (erule rtrancl_induct)
    34.5  txt{*
    34.6  @{subgoals[display,indent=0,margin=65]}
    34.7 -*};
    34.8 +*}
    34.9   apply (rule rtrancl_refl)
   34.10  apply (blast intro: rtrancl_trans)
   34.11  done
   34.12 @@ -112,12 +112,12 @@
   34.13  after intro rules
   34.14  
   34.15  @{subgoals[display,indent=0,margin=65]}
   34.16 -*};
   34.17 +*}
   34.18  apply clarify
   34.19  txt{*
   34.20  after splitting
   34.21  @{subgoals[display,indent=0,margin=65]}
   34.22 -*};
   34.23 +*}
   34.24  oops
   34.25  
   34.26  
   34.27 @@ -127,13 +127,13 @@
   34.28  @{subgoals[display,indent=0,margin=65]}
   34.29  
   34.30  after subsetI
   34.31 -*};
   34.32 +*}
   34.33  apply clarify
   34.34  txt{*
   34.35  @{subgoals[display,indent=0,margin=65]}
   34.36  
   34.37  subgoals after clarify
   34.38 -*};
   34.39 +*}
   34.40  by blast
   34.41  
   34.42  
    35.1 --- a/src/Doc/Tutorial/ToyList/ToyList.thy	Sat Nov 01 11:40:55 2014 +0100
    35.2 +++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Sat Nov 01 14:20:38 2014 +0100
    35.3 @@ -12,7 +12,7 @@
    35.4  *}
    35.5  
    35.6  datatype 'a list = Nil                          ("[]")
    35.7 -                 | Cons 'a "'a list"            (infixr "#" 65);
    35.8 +                 | Cons 'a "'a list"            (infixr "#" 65)
    35.9  
   35.10  text{*\noindent
   35.11  The datatype\index{datatype@\isacommand {datatype} (command)}
   35.12 @@ -140,7 +140,7 @@
   35.13  list.
   35.14  *}
   35.15  
   35.16 -theorem rev_rev [simp]: "rev(rev xs) = xs";
   35.17 +theorem rev_rev [simp]: "rev(rev xs) = xs"
   35.18  
   35.19  txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
   35.20  \noindent
   35.21 @@ -179,7 +179,7 @@
   35.22  nothing obvious except induction on @{term"xs"}:
   35.23  *}
   35.24  
   35.25 -apply(induct_tac xs);
   35.26 +apply(induct_tac xs)
   35.27  
   35.28  txt{*\noindent\index{*induct_tac (method)}%
   35.29  This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
   35.30 @@ -211,7 +211,7 @@
   35.31  Let us try to solve both goals automatically:
   35.32  *}
   35.33  
   35.34 -apply(auto);
   35.35 +apply(auto)
   35.36  
   35.37  txt{*\noindent
   35.38  This command tells Isabelle to apply a proof strategy called
   35.39 @@ -234,7 +234,7 @@
   35.40  \commdx{oops}) we start a new proof:
   35.41  *}
   35.42  
   35.43 -lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   35.44 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
   35.45  
   35.46  txt{*\noindent The keywords \commdx{theorem} and
   35.47  \commdx{lemma} are interchangeable and merely indicate
   35.48 @@ -246,13 +246,13 @@
   35.49  the first argument, @{term"xs"} is the correct one:
   35.50  *}
   35.51  
   35.52 -apply(induct_tac xs);
   35.53 +apply(induct_tac xs)
   35.54  
   35.55  txt{*\noindent
   35.56  This time not even the base case is solved automatically:
   35.57  *}
   35.58  
   35.59 -apply(auto);
   35.60 +apply(auto)
   35.61  
   35.62  txt{*
   35.63  @{subgoals[display,indent=0,goals_limit=1]}
   35.64 @@ -270,9 +270,9 @@
   35.65  We again try the canonical proof procedure:
   35.66  *}
   35.67  
   35.68 -lemma app_Nil2 [simp]: "xs @ [] = xs";
   35.69 -apply(induct_tac xs);
   35.70 -apply(auto);
   35.71 +lemma app_Nil2 [simp]: "xs @ [] = xs"
   35.72 +apply(induct_tac xs)
   35.73 +apply(auto)
   35.74  
   35.75  txt{*
   35.76  \noindent
   35.77 @@ -298,9 +298,9 @@
   35.78  Going back to the proof of the first lemma
   35.79  *}
   35.80  
   35.81 -lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   35.82 -apply(induct_tac xs);
   35.83 -apply(auto);
   35.84 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
   35.85 +apply(induct_tac xs)
   35.86 +apply(auto)
   35.87  
   35.88  txt{*
   35.89  \noindent
   35.90 @@ -324,9 +324,9 @@
   35.91  succeeds without further ado.
   35.92  *}
   35.93  
   35.94 -lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
   35.95 -apply(induct_tac xs);
   35.96 -apply(auto);
   35.97 +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
   35.98 +apply(induct_tac xs)
   35.99 +apply(auto)
  35.100  done
  35.101  
  35.102  text{*
  35.103 @@ -334,18 +334,18 @@
  35.104  Now we can prove the first lemma:
  35.105  *}
  35.106  
  35.107 -lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
  35.108 -apply(induct_tac xs);
  35.109 -apply(auto);
  35.110 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"
  35.111 +apply(induct_tac xs)
  35.112 +apply(auto)
  35.113  done
  35.114  
  35.115  text{*\noindent
  35.116  Finally, we prove our main theorem:
  35.117  *}
  35.118  
  35.119 -theorem rev_rev [simp]: "rev(rev xs) = xs";
  35.120 -apply(induct_tac xs);
  35.121 -apply(auto);
  35.122 +theorem rev_rev [simp]: "rev(rev xs) = xs"
  35.123 +apply(induct_tac xs)
  35.124 +apply(auto)
  35.125  done
  35.126  
  35.127  text{*\noindent
    36.1 --- a/src/Doc/Tutorial/Trie/Trie.thy	Sat Nov 01 11:40:55 2014 +0100
    36.2 +++ b/src/Doc/Tutorial/Trie/Trie.thy	Sat Nov 01 14:20:38 2014 +0100
    36.3 @@ -1,5 +1,5 @@
    36.4  (*<*)
    36.5 -theory Trie imports Main begin;
    36.6 +theory Trie imports Main begin
    36.7  (*>*)
    36.8  text{*
    36.9  To minimize running time, each node of a trie should contain an array that maps
   36.10 @@ -7,9 +7,9 @@
   36.11  representation where the subtries are held in an association list, i.e.\ a
   36.12  list of (letter,trie) pairs.  Abstracting over the alphabet @{typ"'a"} and the
   36.13  values @{typ"'v"} we define a trie as follows:
   36.14 -*};
   36.15 +*}
   36.16  
   36.17 -datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list";
   36.18 +datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list"
   36.19  
   36.20  text{*\noindent
   36.21  \index{datatypes!and nested recursion}%
   36.22 @@ -17,7 +17,7 @@
   36.23  association list of subtries.  This is an example of nested recursion involving products,
   36.24  which is fine because products are datatypes as well.
   36.25  We define two selector functions:
   36.26 -*};
   36.27 +*}
   36.28  
   36.29  primrec "value" :: "('a,'v)trie \<Rightarrow> 'v option" where
   36.30  "value(Trie ov al) = ov"
   36.31 @@ -27,7 +27,7 @@
   36.32  text{*\noindent
   36.33  Association lists come with a generic lookup function.  Its result
   36.34  involves type @{text option} because a lookup can fail:
   36.35 -*};
   36.36 +*}
   36.37  
   36.38  primrec assoc :: "('key * 'val)list \<Rightarrow> 'key \<Rightarrow> 'val option" where
   36.39  "assoc [] x = None" |
   36.40 @@ -39,7 +39,7 @@
   36.41  examining the letters of the search string one by one. As
   36.42  recursion on lists is simpler than on tries, let us express this as primitive
   36.43  recursion on the search string argument:
   36.44 -*};
   36.45 +*}
   36.46  
   36.47  primrec lookup :: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v option" where
   36.48  "lookup t [] = value t" |
   36.49 @@ -51,17 +51,17 @@
   36.50  As a first simple property we prove that looking up a string in the empty
   36.51  trie @{term"Trie None []"} always returns @{const None}. The proof merely
   36.52  distinguishes the two cases whether the search string is empty or not:
   36.53 -*};
   36.54 +*}
   36.55  
   36.56 -lemma [simp]: "lookup (Trie None []) as = None";
   36.57 -apply(case_tac as, simp_all);
   36.58 +lemma [simp]: "lookup (Trie None []) as = None"
   36.59 +apply(case_tac as, simp_all)
   36.60  done
   36.61  
   36.62  text{*
   36.63  Things begin to get interesting with the definition of an update function
   36.64  that adds a new (string, value) pair to a trie, overwriting the old value
   36.65  associated with that string:
   36.66 -*};
   36.67 +*}
   36.68  
   36.69  primrec update:: "('a,'v)trie \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)trie" where
   36.70  "update t []     v = Trie (Some v) (alist t)" |
   36.71 @@ -81,7 +81,7 @@
   36.72  Before we start on any proofs about @{const update} we tell the simplifier to
   36.73  expand all @{text let}s and to split all @{text case}-constructs over
   36.74  options:
   36.75 -*};
   36.76 +*}
   36.77  
   36.78  declare Let_def[simp] option.split[split]
   36.79  
   36.80 @@ -92,10 +92,10 @@
   36.81  
   36.82  Our main goal is to prove the correct interaction of @{const update} and
   36.83  @{const lookup}:
   36.84 -*};
   36.85 +*}
   36.86  
   36.87  theorem "\<forall>t v bs. lookup (update t as v) bs =
   36.88 -                    (if as=bs then Some v else lookup t bs)";
   36.89 +                    (if as=bs then Some v else lookup t bs)"
   36.90  
   36.91  txt{*\noindent
   36.92  Our plan is to induct on @{term as}; hence the remaining variables are
   36.93 @@ -105,8 +105,8 @@
   36.94  if @{const update} has already been simplified, which can only happen if
   36.95  @{term as} is instantiated.
   36.96  The start of the proof is conventional:
   36.97 -*};
   36.98 -apply(induct_tac as, auto);
   36.99 +*}
  36.100 +apply(induct_tac as, auto)
  36.101  
  36.102  txt{*\noindent
  36.103  Unfortunately, this time we are left with three intimidating looking subgoals:
  36.104 @@ -118,8 +118,8 @@
  36.105  Clearly, if we want to make headway we have to instantiate @{term bs} as
  36.106  well now. It turns out that instead of induction, case distinction
  36.107  suffices:
  36.108 -*};
  36.109 -apply(case_tac[!] bs, auto);
  36.110 +*}
  36.111 +apply(case_tac[!] bs, auto)
  36.112  done
  36.113  
  36.114  text{*\noindent
  36.115 @@ -158,7 +158,7 @@
  36.116    with @{typ"'a \<Rightarrow> ('a,'v)trie option"}.
  36.117  \end{exercise}
  36.118  
  36.119 -*};
  36.120 +*}
  36.121  
  36.122  (*<*)
  36.123  
  36.124 @@ -174,9 +174,9 @@
  36.125        in Trie (value t) ((a, update1 tt as vo) # alist t))"
  36.126  
  36.127  theorem [simp]: "\<forall>t v bs. lookup (update1 t as v) bs =
  36.128 -                    (if as = bs then v else lookup t bs)";
  36.129 -apply (induct_tac as, auto);
  36.130 -apply (case_tac[!] bs, auto);
  36.131 +                    (if as = bs then v else lookup t bs)"
  36.132 +apply (induct_tac as, auto)
  36.133 +apply (case_tac[!] bs, auto)
  36.134  done
  36.135  
  36.136  
  36.137 @@ -198,17 +198,17 @@
  36.138       (let tt = (case assoc (alist t) a of 
  36.139                    None \<Rightarrow> Trie None []  
  36.140                  | Some at \<Rightarrow> at) 
  36.141 -      in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))"; 
  36.142 +      in Trie (value t) (overwrite a (update2 tt as vo) (alist t)))" 
  36.143  
  36.144  theorem "\<forall>t v bs. lookup (update2 t as vo) bs =
  36.145 -                    (if as = bs then vo else lookup t bs)";
  36.146 -apply (induct_tac as, auto);
  36.147 -apply (case_tac[!] bs, auto);
  36.148 +                    (if as = bs then vo else lookup t bs)"
  36.149 +apply (induct_tac as, auto)
  36.150 +apply (case_tac[!] bs, auto)
  36.151  done
  36.152  
  36.153  
  36.154  (* Exercise 3. Solution by Getrud Bauer *)
  36.155 -datatype ('a,dead 'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option";
  36.156 +datatype ('a,dead 'v) triem = Triem  "'v option" "'a \<Rightarrow> ('a,'v) triem option"
  36.157  
  36.158  primrec valuem :: "('a, 'v) triem \<Rightarrow> 'v option" where
  36.159  "valuem (Triem ov m) = ov"
  36.160 @@ -220,10 +220,10 @@
  36.161    "lookupm t [] = valuem t" |
  36.162    "lookupm t (a#as) = (case mapping t a of
  36.163                          None \<Rightarrow> None
  36.164 -                      | Some at \<Rightarrow> lookupm at as)";
  36.165 +                      | Some at \<Rightarrow> lookupm at as)"
  36.166  
  36.167 -lemma [simp]: "lookupm (Triem None  (\<lambda>c. None)) as = None";
  36.168 -apply (case_tac as, simp_all);
  36.169 +lemma [simp]: "lookupm (Triem None  (\<lambda>c. None)) as = None"
  36.170 +apply (case_tac as, simp_all)
  36.171  done
  36.172  
  36.173  primrec updatem :: "('a,'v)triem \<Rightarrow> 'a list \<Rightarrow> 'v \<Rightarrow> ('a,'v)triem" where
  36.174 @@ -233,13 +233,13 @@
  36.175                    None \<Rightarrow> Triem None (\<lambda>c. None) 
  36.176                  | Some at \<Rightarrow> at)
  36.177        in Triem (valuem t) 
  36.178 -              (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))";
  36.179 +              (\<lambda>c. if c = a then Some (updatem tt as v) else mapping t c))"
  36.180  
  36.181  theorem "\<forall>t v bs. lookupm (updatem t as v) bs = 
  36.182 -                    (if as = bs then Some v else lookupm t bs)";
  36.183 -apply (induct_tac as, auto);
  36.184 -apply (case_tac[!] bs, auto);
  36.185 +                    (if as = bs then Some v else lookupm t bs)"
  36.186 +apply (induct_tac as, auto)
  36.187 +apply (case_tac[!] bs, auto)
  36.188  done
  36.189  
  36.190 -end;
  36.191 +end
  36.192  (*>*)
    37.1 --- a/src/Doc/Tutorial/Types/Numbers.thy	Sat Nov 01 11:40:55 2014 +0100
    37.2 +++ b/src/Doc/Tutorial/Types/Numbers.thy	Sat Nov 01 14:20:38 2014 +0100
    37.3 @@ -10,7 +10,7 @@
    37.4  lemma "2 * m = m + m"
    37.5  txt{*
    37.6  @{subgoals[display,indent=0,margin=65]}
    37.7 -*};
    37.8 +*}
    37.9  oops
   37.10  
   37.11  fun h :: "nat \<Rightarrow> nat" where
   37.12 @@ -46,11 +46,11 @@
   37.13  lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
   37.14  txt{*
   37.15  @{subgoals[display,indent=0,margin=65]}
   37.16 -*};
   37.17 +*}
   37.18  apply (simp add: ac_simps ac_simps)
   37.19  txt{*
   37.20  @{subgoals[display,indent=0,margin=65]}
   37.21 -*};
   37.22 +*}
   37.23  oops
   37.24  
   37.25  text{*
   37.26 @@ -213,21 +213,21 @@
   37.27  lemma "P ((3/4) * (8/15 :: real))"
   37.28  txt{*
   37.29  @{subgoals[display,indent=0,margin=65]}
   37.30 -*};
   37.31 +*}
   37.32  apply simp 
   37.33  txt{*
   37.34  @{subgoals[display,indent=0,margin=65]}
   37.35 -*};
   37.36 +*}
   37.37  oops
   37.38  
   37.39  lemma "(3/4) * (8/15) < (x :: real)"
   37.40  txt{*
   37.41  @{subgoals[display,indent=0,margin=65]}
   37.42 -*};
   37.43 +*}
   37.44  apply simp 
   37.45  txt{*
   37.46  @{subgoals[display,indent=0,margin=65]}
   37.47 -*};
   37.48 +*}
   37.49  oops
   37.50  
   37.51  text{*
    38.1 --- a/src/Doc/Tutorial/Types/Pairs.thy	Sat Nov 01 11:40:55 2014 +0100
    38.2 +++ b/src/Doc/Tutorial/Types/Pairs.thy	Sat Nov 01 14:20:38 2014 +0100
    38.3 @@ -77,7 +77,7 @@
    38.4  *}
    38.5  
    38.6  lemma "(\<lambda>(x,y).y) p = snd p"
    38.7 -apply(split split_split);
    38.8 +apply(split split_split)
    38.9  
   38.10  txt{*
   38.11  @{subgoals[display,indent=0]}
   38.12 @@ -93,7 +93,7 @@
   38.13  Let us look at a second example:
   38.14  *}
   38.15  
   38.16 -lemma "let (x,y) = p in fst p = x";
   38.17 +lemma "let (x,y) = p in fst p = x"
   38.18  apply(simp only: Let_def)
   38.19  
   38.20  txt{*
   38.21 @@ -189,7 +189,7 @@
   38.22  *}
   38.23  
   38.24  lemma "\<forall>p. \<exists>q. swap p = swap q"
   38.25 -by simp;
   38.26 +by simp
   38.27  
   38.28  text{*\noindent
   38.29  To turn off this automatic splitting, disable the
    39.1 --- a/src/FOLP/ex/Classical.thy	Sat Nov 01 11:40:55 2014 +0100
    39.2 +++ b/src/FOLP/ex/Classical.thy	Sat Nov 01 14:20:38 2014 +0100
    39.3 @@ -145,7 +145,7 @@
    39.4    by (tactic "fast_tac FOLP_cs 1")
    39.5  
    39.6  text "Problem 21"
    39.7 -schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
    39.8 +schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
    39.9    by (tactic "best_tac FOLP_dup_cs 1")
   39.10  
   39.11  text "Problem 22"
   39.12 @@ -173,7 +173,7 @@
   39.13  text "Problem 26"
   39.14  schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
   39.15       (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
   39.16 -  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   39.17 +  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
   39.18    by (tactic "fast_tac FOLP_cs 1")
   39.19  
   39.20  text "Problem 27"
    40.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 11:40:55 2014 +0100
    40.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Nov 01 14:20:38 2014 +0100
    40.3 @@ -33,7 +33,7 @@
    40.4  
    40.5  lemma foldSetD_closed:
    40.6    "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
    40.7 -      |] ==> z \<in> D";
    40.8 +      |] ==> z \<in> D"
    40.9    by (erule foldSetD.cases) auto
   40.10  
   40.11  lemma Diff1_foldSetD:
   40.12 @@ -72,7 +72,7 @@
   40.13    and f_closed [simp, intro!]: "!!x y. [| x \<in> B; y \<in> D |] ==> f x y \<in> D"
   40.14  
   40.15  lemma (in LCD) foldSetD_closed [dest]:
   40.16 -  "(A, z) \<in> foldSetD D f e ==> z \<in> D";
   40.17 +  "(A, z) \<in> foldSetD D f e ==> z \<in> D"
   40.18    by (erule foldSetD.cases) auto
   40.19  
   40.20  lemma (in LCD) Diff1_foldSetD:
    41.1 --- a/src/HOL/Algebra/Module.thy	Sat Nov 01 11:40:55 2014 +0100
    41.2 +++ b/src/HOL/Algebra/Module.thy	Sat Nov 01 14:20:38 2014 +0100
    41.3 @@ -118,7 +118,7 @@
    41.4  qed
    41.5  
    41.6  lemma (in algebra) smult_r_null [simp]:
    41.7 -  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>";
    41.8 +  "a \<in> carrier R ==> a \<odot>\<^bsub>M\<^esub> \<zero>\<^bsub>M\<^esub> = \<zero>\<^bsub>M\<^esub>"
    41.9  proof -
   41.10    assume R: "a \<in> carrier R"
   41.11    note facts = R smult_closed
    42.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Sat Nov 01 11:40:55 2014 +0100
    42.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Sat Nov 01 14:20:38 2014 +0100
    42.3 @@ -508,7 +508,7 @@
    42.4  apply (induct evs, simp)
    42.5  apply (rename_tac a b)
    42.6  apply (case_tac a, simp_all) 
    42.7 -apply (blast dest: parts_trans)+; 
    42.8 +apply (blast dest: parts_trans)+ 
    42.9  done
   42.10  
   42.11  subsubsection{*monotonicity of used*}
    43.1 --- a/src/HOL/Auth/NS_Shared.thy	Sat Nov 01 11:40:55 2014 +0100
    43.2 +++ b/src/HOL/Auth/NS_Shared.thy	Sat Nov 01 14:20:38 2014 +0100
    43.3 @@ -231,7 +231,7 @@
    43.4  apply (drule_tac [8] Says_Server_message_form)
    43.5  apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
    43.6  txt{*NS2, NS3*}
    43.7 -apply blast+; 
    43.8 +apply blast+ 
    43.9  done
   43.10  
   43.11  
   43.12 @@ -468,7 +468,7 @@
   43.13       Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs);
   43.14       Key K \<notin> analz (spies evs);
   43.15       A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk>
   43.16 - \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs";
   43.17 + \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   43.18  apply (erule rev_mp)
   43.19  apply (erule rev_mp)
   43.20  apply (erule rev_mp)
    44.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Sat Nov 01 11:40:55 2014 +0100
    44.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Sat Nov 01 14:20:38 2014 +0100
    44.3 @@ -407,7 +407,7 @@
    44.4  text{*For proving @{text new_keys_not_used}*}
    44.5  lemma keysFor_parts_insert:
    44.6       "\<lbrakk> K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) \<rbrakk>   
    44.7 -      \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H"; 
    44.8 +      \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) \<or> Key (invKey K) \<in> parts H" 
    44.9  by (force 
   44.10      dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
   44.11             analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]
    45.1 --- a/src/HOL/Hoare/Examples.thy	Sat Nov 01 11:40:55 2014 +0100
    45.2 +++ b/src/HOL/Hoare/Examples.thy	Sat Nov 01 14:20:38 2014 +0100
    45.3 @@ -224,7 +224,7 @@
    45.4    OD
    45.5   {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}"
    45.6  (* expand and delete abbreviations first *)
    45.7 -apply (simp);
    45.8 +apply (simp)
    45.9  apply (erule thin_rl)+
   45.10  apply vcg_simp
   45.11     apply (force simp: neq_Nil_conv)
    46.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Sat Nov 01 11:40:55 2014 +0100
    46.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Sat Nov 01 14:20:38 2014 +0100
    46.3 @@ -90,7 +90,7 @@
    46.4  subsubsection{* Graph 2 *}
    46.5  
    46.6  lemma Ex_first_occurrence [rule_format]: 
    46.7 -  "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))";
    46.8 +  "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i. i<m \<longrightarrow> \<not> P i))"
    46.9  apply(rule nat_less_induct)
   46.10  apply clarify
   46.11  apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
    47.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sat Nov 01 11:40:55 2014 +0100
    47.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Sat Nov 01 14:20:38 2014 +0100
    47.3 @@ -220,7 +220,7 @@
    47.4  apply(force intro:tl_of_cptn_is_cptn)
    47.5  done
    47.6  
    47.7 -lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))";
    47.8 +lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"
    47.9  apply(rule nat_less_induct)
   47.10  apply clarify
   47.11  apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m")
    48.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Sat Nov 01 11:40:55 2014 +0100
    48.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Sat Nov 01 14:20:38 2014 +0100
    48.3 @@ -259,7 +259,7 @@
    48.4  qed
    48.5  
    48.6  lemma listset_Rep_Exp_Abs_Exp:
    48.7 -     "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
    48.8 +     "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"
    48.9    by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def)
   48.10  
   48.11  lemma FnCall:
    49.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Sat Nov 01 11:40:55 2014 +0100
    49.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Sat Nov 01 14:20:38 2014 +0100
    49.3 @@ -299,7 +299,7 @@
    49.4    hp a = Some (C,fs) \<longrightarrow> 
    49.5    map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
    49.6    G,hp\<turnstile>v::\<preceq>fd 
    49.7 -  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
    49.8 +  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs"
    49.9  apply (induct frs)
   49.10   apply simp
   49.11  apply clarify
    50.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Sat Nov 01 11:40:55 2014 +0100
    50.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sat Nov 01 14:20:38 2014 +0100
    50.3 @@ -363,7 +363,7 @@
    50.4  theorem sup_state_length [simp]:
    50.5    "G \<turnstile> s2 <=s s1 \<Longrightarrow> 
    50.6     length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
    50.7 -  by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def);
    50.8 +  by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def)
    50.9  
   50.10  theorem sup_state_append_snd:
   50.11    "length a = length b \<Longrightarrow> 
    51.1 --- a/src/HOL/MicroJava/Comp/TypeInf.thy	Sat Nov 01 11:40:55 2014 +0100
    51.2 +++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Sat Nov 01 14:20:38 2014 +0100
    51.3 @@ -10,7 +10,7 @@
    51.4  
    51.5  
    51.6  (**********************************************************************)
    51.7 -;
    51.8 +
    51.9  
   51.10  (*** Inversion of typing rules -- to be moved into WellType.thy
   51.11       Also modify the wtpd_expr_\<dots> proofs in CorrComp.thy ***)
    52.1 --- a/src/HOL/MicroJava/DFA/Err.thy	Sat Nov 01 11:40:55 2014 +0100
    52.2 +++ b/src/HOL/MicroJava/DFA/Err.thy	Sat Nov 01 14:20:38 2014 +0100
    52.3 @@ -117,7 +117,7 @@
    52.4   "OK x <=_(le r) e  =  (e = Err | (? y. e = OK y & x <=_r y))"
    52.5    by (simp add: unfold_lesub_err le_def split: err.split)
    52.6  
    52.7 -lemma top_Err [iff]: "top (le r) Err";
    52.8 +lemma top_Err [iff]: "top (le r) Err"
    52.9    by (simp add: top_def)
   52.10  
   52.11  lemma OK_less_conv [rule_format, iff]:
   52.12 @@ -231,7 +231,7 @@
   52.13  
   52.14  lemma semilat_le_err_OK1:
   52.15    "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
   52.16 -  \<Longrightarrow> x <=_r z";
   52.17 +  \<Longrightarrow> x <=_r z"
   52.18  apply (rule OK_le_err_OK [THEN iffD1])
   52.19  apply (erule subst)
   52.20  apply (simp add: Semilat.ub1 [OF Semilat.intro])
    53.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 11:40:55 2014 +0100
    53.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 14:20:38 2014 +0100
    53.3 @@ -355,7 +355,7 @@
    53.4  apply(simp add: stables_def split_paired_all)
    53.5  apply(rename_tac ss w)
    53.6  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
    53.7 - prefer 2; apply (fast intro: someI)
    53.8 + prefer 2 apply (fast intro: someI)
    53.9  apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
   53.10   prefer 2
   53.11   apply clarify
   53.12 @@ -406,7 +406,7 @@
   53.13  apply(simp add: stables_def split_paired_all)
   53.14  apply(rename_tac ss w)
   53.15  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
   53.16 - prefer 2; apply (fast intro: someI)
   53.17 + prefer 2 apply (fast intro: someI)
   53.18  apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
   53.19   prefer 2
   53.20   apply clarify
    54.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Sat Nov 01 11:40:55 2014 +0100
    54.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Sat Nov 01 14:20:38 2014 +0100
    54.3 @@ -80,7 +80,7 @@
    54.4  done  
    54.5  
    54.6  lemma list_update_le_cong:
    54.7 -  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]";
    54.8 +  "\<lbrakk> i<size xs; xs <=[r] ys; x <=_r y \<rbrakk> \<Longrightarrow> xs[i:=x] <=[r] ys[i:=y]"
    54.9  apply (unfold unfold_lesub_list)
   54.10  apply (unfold Listn.le_def)
   54.11  apply (simp add: list_all2_conv_all_nth nth_list_update)
   54.12 @@ -189,12 +189,12 @@
   54.13  done 
   54.14  
   54.15  lemma Cons_in_list_Suc [iff]:
   54.16 -  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)";
   54.17 +  "(x#xs : list (Suc n) A) = (x\<in> A & xs : list n A)"
   54.18  apply (simp add: in_list_Suc_iff)
   54.19  done 
   54.20  
   54.21  lemma list_not_empty:
   54.22 -  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A";
   54.23 +  "\<exists>a. a\<in> A \<Longrightarrow> \<exists>xs. xs : list n A"
   54.24  apply (induct "n")
   54.25   apply simp
   54.26  apply (simp add: in_list_Suc_iff)
    55.1 --- a/src/HOL/MicroJava/DFA/Opt.thy	Sat Nov 01 11:40:55 2014 +0100
    55.2 +++ b/src/HOL/MicroJava/DFA/Opt.thy	Sat Nov 01 14:20:38 2014 +0100
    55.3 @@ -69,7 +69,7 @@
    55.4  done 
    55.5  
    55.6  lemma le_None [iff]:
    55.7 -  "(ox <=_(le r) None) = (ox = None)";
    55.8 +  "(ox <=_(le r) None) = (ox = None)"
    55.9  apply (unfold lesub_def le_def)
   55.10  apply (simp split: option.split)
   55.11  done 
   55.12 @@ -282,7 +282,7 @@
   55.13  
   55.14  lemma option_map_in_optionI:
   55.15    "\<lbrakk> ox : opt S; !x:S. ox = Some x \<longrightarrow> f x : S \<rbrakk> 
   55.16 -  \<Longrightarrow> map_option f ox : opt S";
   55.17 +  \<Longrightarrow> map_option f ox : opt S"
   55.18  apply (unfold map_option_case)
   55.19  apply (simp split: option.split)
   55.20  apply blast
    56.1 --- a/src/HOL/MicroJava/DFA/Product.thy	Sat Nov 01 11:40:55 2014 +0100
    56.2 +++ b/src/HOL/MicroJava/DFA/Product.thy	Sat Nov 01 14:20:38 2014 +0100
    56.3 @@ -57,7 +57,7 @@
    56.4  
    56.5  lemma closed_lift2_sup:
    56.6    "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
    56.7 -  closed (err(A<*>B)) (lift2(sup f g))";
    56.8 +  closed (err(A<*>B)) (lift2(sup f g))"
    56.9  apply (unfold closed_def plussub_def lift2_def err_def sup_def)
   56.10  apply (simp split: err.split)
   56.11  apply blast
    57.1 --- a/src/HOL/MicroJava/DFA/Semilat.thy	Sat Nov 01 11:40:55 2014 +0100
    57.2 +++ b/src/HOL/MicroJava/DFA/Semilat.thy	Sat Nov 01 14:20:38 2014 +0100
    57.3 @@ -145,7 +145,7 @@
    57.4    (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
    57.5  
    57.6  lemma (in Semilat) lub [simp, intro?]:
    57.7 -  "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z";
    57.8 +  "\<lbrakk> x \<sqsubseteq>\<^sub>r z; y \<sqsubseteq>\<^sub>r z; x \<in> A; y \<in> A; z \<in> A \<rbrakk> \<Longrightarrow> x \<squnion>\<^sub>f y \<sqsubseteq>\<^sub>r z"
    57.9    (*<*) by (insert semilat) (unfold semilat_Def, simp) (*>*)
   57.10  
   57.11  lemma (in Semilat) plus_le_conv [simp]:
   57.12 @@ -299,7 +299,7 @@
   57.13  
   57.14  lemma is_lub_some_lub:
   57.15    "\<lbrakk> single_valued r; acyclic r; (x,u)\<in>r^*; (y,u)\<in>r^* \<rbrakk> 
   57.16 -  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)";
   57.17 +  \<Longrightarrow> is_lub (r^* ) x y (some_lub (r^* ) x y)"
   57.18    (*<*) by (fastforce dest: single_valued_has_lubs simp add: some_lub_conv) (*>*)
   57.19  
   57.20  subsection{*An executable lub-finder*}
   57.21 @@ -331,7 +331,7 @@
   57.22  
   57.23  lemma exec_lub_conv:
   57.24    "\<lbrakk> acyclic r; \<forall>x y. (x,y) \<in> r \<longrightarrow> f x = y; is_lub (r\<^sup>*) x y u \<rbrakk> \<Longrightarrow>
   57.25 -  exec_lub r f x y = u";
   57.26 +  exec_lub r f x y = u"
   57.27  (*<*)
   57.28  apply(unfold exec_lub_def)
   57.29  apply(rule_tac P = "\<lambda>z. (y,z) \<in> r\<^sup>* \<and> (z,u) \<in> r\<^sup>*" and
   57.30 @@ -343,9 +343,9 @@
   57.31     apply(blast dest:rtrancl_into_rtrancl)
   57.32    apply(rename_tac s)
   57.33    apply(subgoal_tac "is_ub (r\<^sup>*) x y s")
   57.34 -   prefer 2; apply(simp add:is_ub_def)
   57.35 +   prefer 2 apply(simp add:is_ub_def)
   57.36    apply(subgoal_tac "(u, s) \<in> r\<^sup>*")
   57.37 -   prefer 2; apply(blast dest:is_lubD)
   57.38 +   prefer 2 apply(blast dest:is_lubD)
   57.39    apply(erule converse_rtranclE)
   57.40     apply blast
   57.41    apply(simp only:acyclic_def)
    58.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Nov 01 11:40:55 2014 +0100
    58.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Sat Nov 01 14:20:38 2014 +0100
    58.3 @@ -357,7 +357,7 @@
    58.4  apply(unfold is_class_def)
    58.5  apply(clarsimp)
    58.6  
    58.7 -apply(rule Call_type_sound);
    58.8 +apply(rule Call_type_sound)
    58.9  prefer 11
   58.10  apply blast
   58.11  apply (simp (no_asm_simp))+ 
    59.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Sat Nov 01 11:40:55 2014 +0100
    59.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Sat Nov 01 14:20:38 2014 +0100
    59.3 @@ -260,9 +260,9 @@
    59.4  done
    59.5  qed
    59.6  
    59.7 -lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
    59.8 +lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma]
    59.9  
   59.10 -lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
   59.11 +lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma]
   59.12  
   59.13  lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); ws_prog G\<rbrakk>
   59.14  \<Longrightarrow> field (G, C) =
    60.1 --- a/src/HOL/NSA/CLim.thy	Sat Nov 01 11:40:55 2014 +0100
    60.2 +++ b/src/HOL/NSA/CLim.thy	Sat Nov 01 14:20:38 2014 +0100
    60.3 @@ -19,7 +19,7 @@
    60.4  by (simp add: numeral_2_eq_2)
    60.5  
    60.6  text{*Changing the quantified variable. Install earlier?*}
    60.7 -lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
    60.8 +lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"
    60.9  apply auto 
   60.10  apply (drule_tac x="x+a" in spec) 
   60.11  apply (simp add: add.assoc) 
    61.1 --- a/src/HOL/NanoJava/TypeRel.thy	Sat Nov 01 11:40:55 2014 +0100
    61.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Sat Nov 01 14:20:38 2014 +0100
    61.3 @@ -114,7 +114,7 @@
    61.4  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    61.5  method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
    61.6  apply (unfold method_def)
    61.7 -apply (erule (1) class_rec [THEN trans]);
    61.8 +apply (erule (1) class_rec [THEN trans])
    61.9  apply simp
   61.10  done
   61.11  
   61.12 @@ -126,7 +126,7 @@
   61.13  lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
   61.14  field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
   61.15  apply (unfold field_def)
   61.16 -apply (erule (1) class_rec [THEN trans]);
   61.17 +apply (erule (1) class_rec [THEN trans])
   61.18  apply simp
   61.19  done
   61.20  
    62.1 --- a/src/HOL/Number_Theory/Cong.thy	Sat Nov 01 11:40:55 2014 +0100
    62.2 +++ b/src/HOL/Number_Theory/Cong.thy	Sat Nov 01 14:20:38 2014 +0100
    62.3 @@ -161,7 +161,7 @@
    62.4  lemma cong_diff_nat:
    62.5    assumes"[a = b] (mod m)" "[c = d] (mod m)" "(a::nat) >= c" "b >= d" 
    62.6    shows "[a - c = b - d] (mod m)"
    62.7 -  using assms by (rule cong_diff_aux_int [transferred]);
    62.8 +  using assms by (rule cong_diff_aux_int [transferred])
    62.9  
   62.10  lemma cong_mult_nat:
   62.11      "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
    63.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Sat Nov 01 11:40:55 2014 +0100
    63.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Sat Nov 01 14:20:38 2014 +0100
    63.3 @@ -765,7 +765,7 @@
    63.4  
    63.5  lemma Fake_parts_insert_in_Un:
    63.6       "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
    63.7 -      ==> Z \<in>  synth (analz H) \<union> parts H";
    63.8 +      ==> Z \<in>  synth (analz H) \<union> parts H"
    63.9  by (blast dest: Fake_parts_insert [THEN subsetD, dest])
   63.10  
   63.11  (*H is sometimes (Key ` KK \<union> spies evs), so can't put G=H*)
   63.12 @@ -906,18 +906,18 @@
   63.13  
   63.14  text{*Two generalizations of @{text analz_insert_eq}*}
   63.15  lemma gen_analz_insert_eq [rule_format]:
   63.16 -     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
   63.17 +     "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
   63.18  by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
   63.19  
   63.20  lemma synth_analz_insert_eq [rule_format]:
   63.21       "X \<in> synth (analz H)
   63.22 -      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
   63.23 +      ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
   63.24  apply (erule synth.induct)
   63.25  apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
   63.26  done
   63.27  
   63.28  lemma Fake_parts_sing:
   63.29 -     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
   63.30 +     "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H"
   63.31  apply (rule subset_trans)
   63.32   apply (erule_tac [2] Fake_parts_insert)
   63.33  apply (simp add: parts_mono)
    64.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Nov 01 11:40:55 2014 +0100
    64.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Sat Nov 01 14:20:38 2014 +0100
    64.3 @@ -131,7 +131,7 @@
    64.4  done
    64.5  
    64.6  lemma above_lemma_b: 
    64.7 -     "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})";
    64.8 +     "acyclic r ==> above i r\<noteq>{}-->(\<exists>j \<in> above i r. above j r = {})"
    64.9  apply (drule above_lemma_a)
   64.10  apply (auto simp add: image0_trancl_iff_image0_r)
   64.11  done
    65.1 --- a/src/Pure/Pure.thy	Sat Nov 01 11:40:55 2014 +0100
    65.2 +++ b/src/Pure/Pure.thy	Sat Nov 01 14:20:38 2014 +0100
    65.3 @@ -105,8 +105,8 @@
    65.4  ML_file "Isar/calculation.ML"
    65.5  ML_file "Tools/bibtex.ML"
    65.6  ML_file "Tools/rail.ML"
    65.7 -ML_file "Tools/rule_insts.ML";
    65.8 -ML_file "Tools/thm_deps.ML";
    65.9 +ML_file "Tools/rule_insts.ML"
   65.10 +ML_file "Tools/thm_deps.ML"
   65.11  ML_file "Tools/class_deps.ML"
   65.12  ML_file "Tools/find_theorems.ML"
   65.13  ML_file "Tools/find_consts.ML"
    66.1 --- a/src/Sequents/LK0.thy	Sat Nov 01 11:40:55 2014 +0100
    66.2 +++ b/src/Sequents/LK0.thy	Sat Nov 01 14:20:38 2014 +0100
    66.3 @@ -359,7 +359,7 @@
    66.4    apply fast
    66.5    done
    66.6  
    66.7 -lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y";
    66.8 +lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"
    66.9    apply (unfold If_def)
   66.10    apply (erule thinR [THEN cut])
   66.11    apply fast
    67.1 --- a/src/ZF/AC/AC16_WO4.thy	Sat Nov 01 11:40:55 2014 +0100
    67.2 +++ b/src/ZF/AC/AC16_WO4.thy	Sat Nov 01 14:20:38 2014 +0100
    67.3 @@ -45,7 +45,7 @@
    67.4  (* There exists a well ordered set y such that ...                        *)
    67.5  (* ********************************************************************** *)
    67.6  
    67.7 -lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll];
    67.8 +lemmas lepoll_paired = paired_eqpoll [THEN eqpoll_sym, THEN eqpoll_imp_lepoll]
    67.9  
   67.10  lemma lemma2: "\<exists>y R. well_ord(y,R) & x \<inter> y = 0 & ~y \<lesssim> z & ~Finite(y)"
   67.11  apply (rule_tac x = "{{a,x}. a \<in> nat \<union> Hartog (z) }" in exI)
    68.1 --- a/src/ZF/AC/WO2_AC16.thy	Sat Nov 01 11:40:55 2014 +0100
    68.2 +++ b/src/ZF/AC/WO2_AC16.thy	Sat Nov 01 14:20:38 2014 +0100
    68.3 @@ -309,13 +309,13 @@
    68.4  apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 
    68.5  apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)  
    68.6  apply (blast intro: Card_is_Ord) 
    68.7 -done;
    68.8 +done
    68.9  
   68.10  (* back to the proof *)
   68.11  
   68.12  lemmas disj_Un_eqpoll_nat_sum = 
   68.13      eqpoll_trans [THEN eqpoll_trans, 
   68.14 -                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum];
   68.15 +                  OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]
   68.16  
   68.17  
   68.18  lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;   
    69.1 --- a/src/ZF/Arith.thy	Sat Nov 01 11:40:55 2014 +0100
    69.2 +++ b/src/ZF/Arith.thy	Sat Nov 01 14:20:38 2014 +0100
    69.3 @@ -413,12 +413,12 @@
    69.4      "i \<in> nat ==> pred(i) \<in> nat"
    69.5  by (simp add: pred_def split: split_nat_case)
    69.6  
    69.7 -lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)";
    69.8 +lemma nat_diff_pred: "[|i\<in>nat; j\<in>nat|] ==> i #- succ(j) = pred(i #- j)"
    69.9  apply (rule_tac m=i and n=j in diff_induct)
   69.10  apply (auto simp add: pred_def nat_imp_quasinat split: split_nat_case)
   69.11  done
   69.12  
   69.13 -lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)";
   69.14 +lemma diff_succ_eq_pred: "i #- succ(j) = pred(i #- j)"
   69.15  apply (insert nat_diff_pred [of "natify(i)" "natify(j)"])
   69.16  apply (simp add: natify_succ [symmetric])
   69.17  done
   69.18 @@ -435,7 +435,7 @@
   69.19  
   69.20  text{*We actually prove @{term "i #- j #- k = i #- (j #+ k)"}*}
   69.21  lemma diff_diff_left [simplified]:
   69.22 -     "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)";
   69.23 +     "natify(i)#-natify(j)#-k = natify(i) #- (natify(j)#+k)"
   69.24  by (rule_tac m="natify(i)" and n="natify(j)" in diff_induct, auto)
   69.25  
   69.26  
    70.1 --- a/src/ZF/Coind/Values.thy	Sat Nov 01 11:40:55 2014 +0100
    70.2 +++ b/src/ZF/Coind/Values.thy	Sat Nov 01 14:20:38 2014 +0100
    70.3 @@ -10,7 +10,7 @@
    70.4  consts
    70.5    Val  :: i
    70.6    ValEnv  :: i
    70.7 -  Val_ValEnv  :: i;
    70.8 +  Val_ValEnv  :: i
    70.9  
   70.10  codatatype
   70.11      "Val" = v_const ("c \<in> Const")
    71.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Sat Nov 01 11:40:55 2014 +0100
    71.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Sat Nov 01 14:20:38 2014 +0100
    71.3 @@ -969,7 +969,7 @@
    71.4             "M(g) ==>
    71.5              strong_replacement
    71.6                (M, \<lambda>x y. x \<in> formula &
    71.7 -                  y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)";
    71.8 +                  y = \<langle>x, formula_rec_case(a,b,c,d,g,x)\<rangle>)"
    71.9  
   71.10  lemma (in Formula_Rec) formula_rec_case_closed:
   71.11      "[|M(g); p \<in> formula|] ==> M(formula_rec_case(a, b, c, d, g, p))"
    72.1 --- a/src/ZF/Constructible/Formula.thy	Sat Nov 01 11:40:55 2014 +0100
    72.2 +++ b/src/ZF/Constructible/Formula.thy	Sat Nov 01 14:20:38 2014 +0100
    72.3 @@ -42,7 +42,7 @@
    72.4  
    72.5  definition
    72.6    Exists :: "i=>i" where
    72.7 -  "Exists(p) == Neg(Forall(Neg(p)))";
    72.8 +  "Exists(p) == Neg(Forall(Neg(p)))"
    72.9  
   72.10  lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
   72.11  by (simp add: Neg_def)
   72.12 @@ -107,7 +107,7 @@
   72.13     ==> sats(A, Forall(p), env) \<longleftrightarrow> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
   72.14  by simp
   72.15  
   72.16 -declare satisfies.simps [simp del];
   72.17 +declare satisfies.simps [simp del]
   72.18  
   72.19  subsection{*Dividing line between primitive and derived connectives*}
   72.20  
   72.21 @@ -601,10 +601,10 @@
   72.22  lemma Lset: "Lset(i) = (\<Union>j\<in>i. DPow(Lset(j)))"
   72.23  by (subst Lset_def [THEN def_transrec], simp)
   72.24  
   72.25 -lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)";
   72.26 +lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)"
   72.27  by (subst Lset, blast)
   72.28  
   72.29 -lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))";
   72.30 +lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))"
   72.31  apply (insert Lset [of x])
   72.32  apply (blast intro: elim: equalityE)
   72.33  done
   72.34 @@ -888,7 +888,7 @@
   72.35  declare Ord_lrank [THEN lrank_of_Ord, simp]
   72.36  
   72.37  text{*Kunen's VI 1.10 *}
   72.38 -lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))";
   72.39 +lemma Lset_in_Lset_succ: "Lset(i) \<in> Lset(succ(i))"
   72.40  apply (simp add: Lset_succ DPow_def)
   72.41  apply (rule_tac x=Nil in bexI)
   72.42   apply (rule_tac x="Equal(0,0)" in bexI)
   72.43 @@ -907,7 +907,7 @@
   72.44  done
   72.45  
   72.46  text{*Kunen's VI 1.11 *}
   72.47 -lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)";
   72.48 +lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)"
   72.49  apply (erule trans_induct)
   72.50  apply (subst Lset)
   72.51  apply (subst Vset)
   72.52 @@ -917,7 +917,7 @@
   72.53  done
   72.54  
   72.55  text{*Kunen's VI 1.12 *}
   72.56 -lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)";
   72.57 +lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)"
   72.58  apply (erule nat_induct)
   72.59   apply (simp add: Vfrom_0)
   72.60  apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
   72.61 @@ -1002,7 +1002,7 @@
   72.62                  \<exists>env \<in> list(A). \<exists>p \<in> formula.
   72.63                      X = {x\<in>A. sats(A, p, Cons(x,env))}}"
   72.64  
   72.65 -lemma DPow_subset_DPow': "DPow(A) \<subseteq> DPow'(A)";
   72.66 +lemma DPow_subset_DPow': "DPow(A) \<subseteq> DPow'(A)"
   72.67  by (simp add: DPow_def DPow'_def, blast)
   72.68  
   72.69  lemma DPow'_0: "DPow'(0) = {0}"
    73.1 --- a/src/ZF/Constructible/Rank.thy	Sat Nov 01 11:40:55 2014 +0100
    73.2 +++ b/src/ZF/Constructible/Rank.thy	Sat Nov 01 14:20:38 2014 +0100
    73.3 @@ -566,7 +566,7 @@
    73.4  subsubsection{*Ordinal Multiplication*}
    73.5  
    73.6  lemma omult_eqns_unique:
    73.7 -     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";
    73.8 +     "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'"
    73.9  apply (simp add: omult_eqns_def, clarify) 
   73.10  apply (erule Ord_cases, simp_all) 
   73.11  done
    74.1 --- a/src/ZF/Constructible/Reflection.thy	Sat Nov 01 11:40:55 2014 +0100
    74.2 +++ b/src/ZF/Constructible/Reflection.thy	Sat Nov 01 14:20:38 2014 +0100
    74.3 @@ -6,10 +6,10 @@
    74.4  
    74.5  theory Reflection imports Normal begin
    74.6  
    74.7 -lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))";
    74.8 +lemma all_iff_not_ex_not: "(\<forall>x. P(x)) \<longleftrightarrow> (~ (\<exists>x. ~ P(x)))"
    74.9  by blast
   74.10  
   74.11 -lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))";
   74.12 +lemma ball_iff_not_bex_not: "(\<forall>x\<in>A. P(x)) \<longleftrightarrow> (~ (\<exists>x\<in>A. ~ P(x)))"
   74.13  by blast
   74.14  
   74.15  text{*From the notes of A. S. Kechris, page 6, and from
   74.16 @@ -339,14 +339,14 @@
   74.17  schematic_lemma (in reflection)
   74.18       "Reflects(?Cl,
   74.19                 \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
   74.20 -               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
   74.21 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))"
   74.22  by fast
   74.23  
   74.24  text{*Example 3''*}
   74.25  schematic_lemma (in reflection)
   74.26       "Reflects(?Cl,
   74.27                 \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
   74.28 -               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
   74.29 +               \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))"
   74.30  by fast
   74.31  
   74.32  text{*Example 4: Axiom of Choice.  Possibly wrong, since @{text \<Pi>} needs
    75.1 --- a/src/ZF/Constructible/Relative.thy	Sat Nov 01 11:40:55 2014 +0100
    75.2 +++ b/src/ZF/Constructible/Relative.thy	Sat Nov 01 14:20:38 2014 +0100
    75.3 @@ -1336,7 +1336,7 @@
    75.4  text{*The assumption @{term "M(A->B)"} is unusual, but essential: in
    75.5  all but trivial cases, A->B cannot be expected to belong to @{term M}.*}
    75.6  lemma (in M_basic) is_funspace_abs [simp]:
    75.7 -     "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B";
    75.8 +     "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B"
    75.9  apply (simp add: is_funspace_def)
   75.10  apply (rule iffI)
   75.11   prefer 2 apply blast
    76.1 --- a/src/ZF/Constructible/WFrec.thy	Sat Nov 01 11:40:55 2014 +0100
    76.2 +++ b/src/ZF/Constructible/WFrec.thy	Sat Nov 01 14:20:38 2014 +0100
    76.3 @@ -135,7 +135,7 @@
    76.4    "[| M(r); M(f); \<forall>x[M]. \<forall>g[M]. function(g) \<longrightarrow> M(H(x,g)) |] 
    76.5     ==> is_recfun(r,a,H,f) \<longleftrightarrow>
    76.6         (\<forall>z[M]. z \<in> f \<longleftrightarrow> 
    76.7 -        (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))";
    76.8 +        (\<exists>x[M]. <x,a> \<in> r & z = <x, H(x, restrict(f, r-``{x}))>))"
    76.9  apply (simp add: is_recfun_def lam_def)
   76.10  apply (safe intro!: equalityI) 
   76.11     apply (drule equalityD1 [THEN subsetD], assumption) 
    77.1 --- a/src/ZF/Epsilon.thy	Sat Nov 01 11:40:55 2014 +0100
    77.2 +++ b/src/ZF/Epsilon.thy	Sat Nov 01 14:20:38 2014 +0100
    77.3 @@ -117,14 +117,14 @@
    77.4  done
    77.5  
    77.6  text{*A transitive set either is empty or contains the empty set.*}
    77.7 -lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
    77.8 +lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A"
    77.9  apply (simp add: Transset_def)
   77.10  apply (rule_tac a=x in eps_induct, clarify)
   77.11  apply (drule bspec, assumption)
   77.12  apply (case_tac "x=0", auto)
   77.13  done
   77.14  
   77.15 -lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
   77.16 +lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A"
   77.17  by (blast dest: Transset_0_lemma)
   77.18  
   77.19  
    78.1 --- a/src/ZF/List_ZF.thy	Sat Nov 01 11:40:55 2014 +0100
    78.2 +++ b/src/ZF/List_ZF.thy	Sat Nov 01 14:20:38 2014 +0100
    78.3 @@ -1216,7 +1216,7 @@
    78.4  lemma sublist_upt_eq_take [rule_format, simp]:
    78.5      "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
    78.6  apply (erule list.induct, simp)
    78.7 -apply (clarify );
    78.8 +apply (clarify )
    78.9  apply (erule natE)
   78.10  apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
   78.11  done
    79.1 --- a/src/ZF/Nat_ZF.thy	Sat Nov 01 11:40:55 2014 +0100
    79.2 +++ b/src/ZF/Nat_ZF.thy	Sat Nov 01 14:20:38 2014 +0100
    79.3 @@ -244,7 +244,7 @@
    79.4  
    79.5  lemma nat_case_type [TC]:
    79.6      "[| n \<in> nat;  a \<in> C(0);  !!m. m \<in> nat ==> b(m): C(succ(m)) |]
    79.7 -     ==> nat_case(a,b,n) \<in> C(n)";
    79.8 +     ==> nat_case(a,b,n) \<in> C(n)"
    79.9  by (erule nat_induct, auto)
   79.10  
   79.11  lemma split_nat_case:
    80.1 --- a/src/ZF/OrdQuant.thy	Sat Nov 01 11:40:55 2014 +0100
    80.2 +++ b/src/ZF/OrdQuant.thy	Sat Nov 01 14:20:38 2014 +0100
    80.3 @@ -273,7 +273,7 @@
    80.4  lemma rex_is_bex [simp]: "(\<exists>x[%z. z\<in>A]. P(x)) <-> (\<exists>x\<in>A. P(x))"
    80.5  by blast
    80.6  
    80.7 -lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))";
    80.8 +lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (\<forall>x[M]. P(x))"
    80.9  by (simp add: rall_def atomize_all atomize_imp)
   80.10  
   80.11  declare atomize_rall [symmetric, rulify]
    81.1 --- a/src/ZF/Sum.thy	Sat Nov 01 11:40:55 2014 +0100
    81.2 +++ b/src/ZF/Sum.thy	Sat Nov 01 14:20:38 2014 +0100
    81.3 @@ -109,10 +109,10 @@
    81.4  lemma sum_iff: "u \<in> A+B \<longleftrightarrow> (\<exists>x. x \<in> A & u=Inl(x)) | (\<exists>y. y \<in> B & u=Inr(y))"
    81.5  by blast
    81.6  
    81.7 -lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)";
    81.8 +lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) \<longleftrightarrow> (x \<in> A)"
    81.9  by auto
   81.10  
   81.11 -lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)";
   81.12 +lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) \<longleftrightarrow> (y \<in> B)"
   81.13  by auto
   81.14  
   81.15  lemma sum_subset_iff: "A+B \<subseteq> C+D \<longleftrightarrow> A<=C & B<=D"
    82.1 --- a/src/ZF/Trancl.thy	Sat Nov 01 11:40:55 2014 +0100
    82.2 +++ b/src/ZF/Trancl.thy	Sat Nov 01 14:20:38 2014 +0100
    82.3 @@ -90,7 +90,7 @@
    82.4  lemma trans_imp_trans_on: "trans(r) ==> trans[A](r)"
    82.5  by (unfold trans_def trans_on_def, blast)
    82.6  
    82.7 -lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)";
    82.8 +lemma trans_on_imp_trans: "[|trans[A](r); r \<subseteq> A*A|] ==> trans(r)"
    82.9  by (simp add: trans_on_def trans_def, blast)
   82.10  
   82.11  
    83.1 --- a/src/ZF/UNITY/AllocImpl.thy	Sat Nov 01 11:40:55 2014 +0100
    83.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Sat Nov 01 14:20:38 2014 +0100
    83.3 @@ -415,7 +415,7 @@
    83.4   prefer 2 apply (force)
    83.5  apply (subgoal_tac "x`available_tok =
    83.6                      NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
    83.7 -apply (simp add: );
    83.8 +apply (simp add: )
    83.9  apply (auto split add: nat_diff_split dest: lt_trans2)
   83.10  done
   83.11  
    84.1 --- a/src/ZF/UNITY/ClientImpl.thy	Sat Nov 01 11:40:55 2014 +0100
    84.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Sat Nov 01 14:20:38 2014 +0100
    84.3 @@ -105,14 +105,14 @@
    84.4  
    84.5  
    84.6  lemma preserves_lift_imp_stable:
    84.7 -     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
    84.8 +     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
    84.9  apply (drule preserves_imp_stable)
   84.10  apply (simp add: lift_def)
   84.11  done
   84.12  
   84.13  lemma preserves_imp_prefix:
   84.14       "G \<in> preserves(lift(ff))
   84.15 -      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
   84.16 +      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
   84.17  by (erule preserves_lift_imp_stable)
   84.18  
   84.19  (*Safety property 1 \<in> ask, rel are increasing: (24) *)
    85.1 --- a/src/ZF/Univ.thy	Sat Nov 01 11:40:55 2014 +0100
    85.2 +++ b/src/ZF/Univ.thy	Sat Nov 01 14:20:38 2014 +0100
    85.3 @@ -453,7 +453,7 @@
    85.4                      Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
    85.5  done
    85.6  
    85.7 -lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
    85.8 +lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))"
    85.9  apply (erule nat_induct)
   85.10   apply (simp add: Vfrom_0)
   85.11  apply (simp add: Vset_succ)
    86.1 --- a/src/ZF/equalities.thy	Sat Nov 01 11:40:55 2014 +0100
    86.2 +++ b/src/ZF/equalities.thy	Sat Nov 01 14:20:38 2014 +0100
    86.3 @@ -22,10 +22,10 @@
    86.4    The following are not added to the default simpset because
    86.5    (a) they duplicate the body and (b) there are no similar rules for @{text Int}.*}
    86.6  
    86.7 -lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))";
    86.8 +lemma ball_Un: "(\<forall>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<forall>x \<in> A. P(x)) & (\<forall>x \<in> B. P(x))"
    86.9    by blast
   86.10  
   86.11 -lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))";
   86.12 +lemma bex_Un: "(\<exists>x \<in> A\<union>B. P(x)) \<longleftrightarrow> (\<exists>x \<in> A. P(x)) | (\<exists>x \<in> B. P(x))"
   86.13    by blast
   86.14  
   86.15  lemma ball_UN: "(\<forall>z \<in> (\<Union>x\<in>A. B(x)). P(z)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>z \<in> B(x). P(z))"
    87.1 --- a/src/ZF/ex/Group.thy	Sat Nov 01 11:40:55 2014 +0100
    87.2 +++ b/src/ZF/ex/Group.thy	Sat Nov 01 14:20:38 2014 +0100
    87.3 @@ -383,7 +383,7 @@
    87.4  apply (subgoal_tac "converse(h) \<in> carrier(H) \<rightarrow> carrier(G)")
    87.5   prefer 2 apply (simp add: bij_converse_bij bij_is_fun)
    87.6  apply (auto intro: left_inverse_eq [of _ "carrier(G)" "carrier(H)"]
    87.7 -            simp add: hom_def bij_is_inj right_inverse_bij);
    87.8 +            simp add: hom_def bij_is_inj right_inverse_bij)
    87.9  done
   87.10  
   87.11  lemma (in group) iso_trans:
   87.12 @@ -658,7 +658,7 @@
   87.13    by (simp add: normal_def subgroup_def)
   87.14  
   87.15  lemma (in group) normalI:
   87.16 -  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G";
   87.17 +  "subgroup(H,G) \<Longrightarrow> (\<forall>x \<in> carrier(G). H #> x = x <# H) \<Longrightarrow> H \<lhd> G"
   87.18    by (simp add: normal_def normal_axioms_def)
   87.19  
   87.20  lemma (in normal) inv_op_closed1:
   87.21 @@ -1086,7 +1086,7 @@
   87.22  definition
   87.23    kernel :: "[i,i,i] => i" where
   87.24      --{*the kernel of a homomorphism*}
   87.25 -  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
   87.26 +  "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}"
   87.27  
   87.28  lemma (in group_hom) subgroup_kernel: "subgroup (kernel(G,H,h), G)"
   87.29  apply (rule subgroup.intro)
    88.1 --- a/src/ZF/ex/LList.thy	Sat Nov 01 11:40:55 2014 +0100
    88.2 +++ b/src/ZF/ex/LList.thy	Sat Nov 01 14:20:38 2014 +0100
    88.3 @@ -16,7 +16,7 @@
    88.4  theory LList imports Main begin
    88.5  
    88.6  consts
    88.7 -  llist  :: "i=>i";
    88.8 +  llist  :: "i=>i"
    88.9  
   88.10  codatatype
   88.11    "llist(A)" = LNil | LCons ("a \<in> A", "l \<in> llist(A)")
    89.1 --- a/src/ZF/func.thy	Sat Nov 01 11:40:55 2014 +0100
    89.2 +++ b/src/ZF/func.thy	Sat Nov 01 14:20:38 2014 +0100
    89.3 @@ -249,7 +249,7 @@
    89.4  
    89.5  lemma Repfun_function_if:
    89.6       "function(f)
    89.7 -      ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))";
    89.8 +      ==> {f`x. x \<in> C} = (if C \<subseteq> domain(f) then f``C else cons(0,f``C))"
    89.9  apply simp
   89.10  apply (intro conjI impI)
   89.11   apply (blast dest: function_apply_equality intro: function_apply_Pair)
   89.12 @@ -261,7 +261,7 @@
   89.13  (*For this lemma and the next, the right-hand side could equivalently
   89.14    be written \<Union>x\<in>C. {f`x} *)
   89.15  lemma image_function:
   89.16 -     "[| function(f);  C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}";
   89.17 +     "[| function(f);  C \<subseteq> domain(f) |] ==> f``C = {f`x. x \<in> C}"
   89.18  by (simp add: Repfun_function_if)
   89.19  
   89.20  lemma image_fun: "[| f \<in> Pi(A,B);  C \<subseteq> A |] ==> f``C = {f`x. x \<in> C}"