1.1 --- a/doc-src/TutorialI/Advanced/Partial.thy Fri Jan 18 17:46:17 2002 +0100
1.2 +++ b/doc-src/TutorialI/Advanced/Partial.thy Fri Jan 18 18:30:19 2002 +0100
1.3 @@ -138,7 +138,7 @@
1.4 *}
1.5
1.6 lemma "wf(step1 f) \<longrightarrow> f(find(f,x)) = find(f,x)"
1.7 -apply(induct_tac f x rule:find.induct);
1.8 +apply(induct_tac f x rule: find.induct);
1.9 apply simp
1.10 done
1.11
1.12 @@ -193,7 +193,7 @@
1.13 apply(rule_tac P = "\<lambda>(x,x'). x' = f x" and
1.14 r = "inv_image (step1 f) fst" in while_rule);
1.15 apply auto
1.16 -apply(simp add:inv_image_def step1_def)
1.17 +apply(simp add: inv_image_def step1_def)
1.18 done
1.19
1.20 text{*
1.21 @@ -202,7 +202,7 @@
1.22
1.23 theorem "wf(step1 f) \<Longrightarrow> f(find2 f x) = find2 f x"
1.24 apply(drule_tac x = x in lem)
1.25 -apply(auto simp add:find2_def)
1.26 +apply(auto simp add: find2_def)
1.27 done
1.28
1.29 text{* Let us conclude this section on partial functions by a
2.1 --- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 18 17:46:17 2002 +0100
2.2 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri Jan 18 18:30:19 2002 +0100
2.3 @@ -165,7 +165,7 @@
2.4 \isamarkuptrue%
2.5 \isacommand{lemma}\ {\isachardoublequote}wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\ {\isasymlongrightarrow}\ f{\isacharparenleft}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isanewline
2.6 \isamarkupfalse%
2.7 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}find{\isachardot}induct{\isacharparenright}\isanewline
2.8 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f\ x\ rule{\isacharcolon}\ find{\isachardot}induct{\isacharparenright}\isanewline
2.9 \isamarkupfalse%
2.10 \isacommand{apply}\ simp\isanewline
2.11 \isamarkupfalse%
2.12 @@ -236,7 +236,7 @@
2.13 \isamarkupfalse%
2.14 \isacommand{apply}\ auto\isanewline
2.15 \isamarkupfalse%
2.16 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
2.17 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ inv{\isacharunderscore}image{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}\isanewline
2.18 \isamarkupfalse%
2.19 \isacommand{done}\isamarkupfalse%
2.20 %
2.21 @@ -248,7 +248,7 @@
2.22 \isamarkupfalse%
2.23 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ lem{\isacharparenright}\isanewline
2.24 \isamarkupfalse%
2.25 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
2.26 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ find{\isadigit{2}}{\isacharunderscore}def{\isacharparenright}\isanewline
2.27 \isamarkupfalse%
2.28 \isacommand{done}\isamarkupfalse%
2.29 %
3.1 --- a/doc-src/TutorialI/CTL/CTL.thy Fri Jan 18 17:46:17 2002 +0100
3.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Jan 18 18:30:19 2002 +0100
3.3 @@ -31,7 +31,8 @@
3.4 This definition allows a succinct statement of the semantics of @{term AF}:
3.5 \footnote{Do not be misled: neither datatypes nor recursive functions can be
3.6 extended by new constructors or equations. This is just a trick of the
3.7 -presentation. In reality one has to define a new datatype and a new function.}
3.8 +presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
3.9 +a new datatype and a new function.}
3.10 *};
3.11 (*<*)
3.12 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
3.13 @@ -165,7 +166,7 @@
3.14 "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
3.15 apply(erule contrapos_np);
3.16 apply(subst lfp_unfold[OF mono_af]);
3.17 -apply(simp add:af_def);
3.18 +apply(simp add: af_def);
3.19 done;
3.20
3.21 text{*\noindent
3.22 @@ -210,7 +211,7 @@
3.23 From this proposition the original goal follows easily:
3.24 *};
3.25
3.26 - apply(simp add:Paths_def, blast);
3.27 + apply(simp add: Paths_def, blast);
3.28
3.29 txt{*\noindent
3.30 The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}:
3.31 @@ -242,7 +243,7 @@
3.32 @{text fast} can prove the base case quickly:
3.33 *};
3.34
3.35 - apply(fast intro:someI2_ex);
3.36 + apply(fast intro: someI2_ex);
3.37
3.38 txt{*\noindent
3.39 What is worth noting here is that we have used \methdx{fast} rather than
3.40 @@ -285,14 +286,14 @@
3.41 \<exists> p\<in>Paths s. \<forall> i. Q(p i)";
3.42 apply(subgoal_tac
3.43 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");
3.44 - apply(simp add:Paths_def);
3.45 + apply(simp add: Paths_def);
3.46 apply(blast);
3.47 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI);
3.48 apply(simp);
3.49 apply(intro strip);
3.50 apply(induct_tac i);
3.51 apply(simp);
3.52 - apply(fast intro:someI2_ex);
3.53 + apply(fast intro: someI2_ex);
3.54 apply(simp);
3.55 apply(rule someI2_ex);
3.56 apply(blast);
3.57 @@ -328,7 +329,7 @@
3.58 Both are solved automatically:
3.59 *};
3.60
3.61 - apply(auto dest:not_in_lfp_afD);
3.62 + apply(auto dest: not_in_lfp_afD);
3.63 done;
3.64
3.65 text{*
3.66 @@ -388,7 +389,7 @@
3.67
3.68 lemma "lfp(eufix A B) \<subseteq> eusem A B"
3.69 apply(rule lfp_lowerbound)
3.70 -apply(clarsimp simp add:eusem_def eufix_def);
3.71 +apply(clarsimp simp add: eusem_def eufix_def);
3.72 apply(erule disjE);
3.73 apply(rule_tac x = "[]" in exI);
3.74 apply simp
3.75 @@ -403,15 +404,15 @@
3.76 done
3.77
3.78 lemma "eusem A B \<subseteq> lfp(eufix A B)";
3.79 -apply(clarsimp simp add:eusem_def);
3.80 +apply(clarsimp simp add: eusem_def);
3.81 apply(erule rev_mp);
3.82 apply(rule_tac x = x in spec);
3.83 apply(induct_tac p);
3.84 apply(subst lfp_unfold[OF mono_eufix])
3.85 - apply(simp add:eufix_def);
3.86 + apply(simp add: eufix_def);
3.87 apply(clarsimp);
3.88 apply(subst lfp_unfold[OF mono_eufix])
3.89 -apply(simp add:eufix_def);
3.90 +apply(simp add: eufix_def);
3.91 apply blast;
3.92 done
3.93
3.94 @@ -429,7 +430,7 @@
3.95 "apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
3.96
3.97 lemma [iff]: "apath s \<in> Paths s";
3.98 -apply(simp add:Paths_def);
3.99 +apply(simp add: Paths_def);
3.100 apply(blast intro: M_total[THEN someI_ex])
3.101 done
3.102
3.103 @@ -438,11 +439,11 @@
3.104 "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
3.105
3.106 lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
3.107 -by(simp add:Paths_def pcons_def split:nat.split);
3.108 +by(simp add: Paths_def pcons_def split: nat.split);
3.109
3.110 lemma "lfp(eufix A B) \<subseteq> eusem A B"
3.111 apply(rule lfp_lowerbound)
3.112 -apply(clarsimp simp add:eusem_def eufix_def);
3.113 +apply(clarsimp simp add: eusem_def eufix_def);
3.114 apply(erule disjE);
3.115 apply(rule_tac x = "apath x" in bexI);
3.116 apply(rule_tac x = 0 in exI);
3.117 @@ -451,8 +452,8 @@
3.118 apply(clarify);
3.119 apply(rule_tac x = "pcons xb p" in bexI);
3.120 apply(rule_tac x = "j+1" in exI);
3.121 - apply (simp add:pcons_def split:nat.split);
3.122 -apply (simp add:pcons_PathI)
3.123 + apply (simp add: pcons_def split: nat.split);
3.124 +apply (simp add: pcons_PathI)
3.125 done
3.126 *)
3.127 (*>*)
4.1 --- a/doc-src/TutorialI/CTL/CTLind.thy Fri Jan 18 17:46:17 2002 +0100
4.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy Fri Jan 18 18:30:19 2002 +0100
4.3 @@ -47,7 +47,7 @@
4.4 apply(blast);
4.5 apply(clarify);
4.6 apply(drule_tac x = "\<lambda>i. case i of 0 \<Rightarrow> t | Suc i \<Rightarrow> f i" in bspec);
4.7 -apply(simp_all add:Paths_def split:nat.split);
4.8 +apply(simp_all add: Paths_def split: nat.split);
4.9 done
4.10
4.11 text{*\noindent
4.12 @@ -106,7 +106,7 @@
4.13
4.14 apply(subst lfp_unfold[OF mono_af]);
4.15 apply(simp (no_asm) add: af_def);
4.16 - apply(blast intro:Avoid.intros);
4.17 + apply(blast intro: Avoid.intros);
4.18
4.19 txt{*
4.20 Having proved the main goal, we return to the proof obligation that the
4.21 @@ -120,10 +120,10 @@
4.22 *}
4.23
4.24 apply(erule contrapos_pp);
4.25 -apply(simp add:wf_iff_no_infinite_down_chain);
4.26 +apply(simp add: wf_iff_no_infinite_down_chain);
4.27 apply(erule exE);
4.28 apply(rule ex_infinite_path);
4.29 -apply(auto simp add:Paths_def);
4.30 +apply(auto simp add: Paths_def);
4.31 done
4.32
4.33 text{*
4.34 @@ -140,7 +140,7 @@
4.35 \index{CTL|)}*}
4.36
4.37 theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
4.38 -by(auto elim:Avoid_in_lfp intro:Avoid.intros);
4.39 +by(auto elim: Avoid_in_lfp intro: Avoid.intros);
4.40
4.41
4.42 (*<*)end(*>*)
5.1 --- a/doc-src/TutorialI/CTL/PDL.thy Fri Jan 18 17:46:17 2002 +0100
5.2 +++ b/doc-src/TutorialI/CTL/PDL.thy Fri Jan 18 18:30:19 2002 +0100
5.3 @@ -174,7 +174,7 @@
5.4
5.5 theorem "mc f = {s. s \<Turnstile> f}"
5.6 apply(induct_tac f)
5.7 -apply(auto simp add:EF_lemma)
5.8 +apply(auto simp add: EF_lemma)
5.9 done
5.10
5.11 text{*
6.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 18 17:46:17 2002 +0100
6.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 18 18:30:19 2002 +0100
6.3 @@ -34,7 +34,8 @@
6.4 This definition allows a succinct statement of the semantics of \isa{AF}:
6.5 \footnote{Do not be misled: neither datatypes nor recursive functions can be
6.6 extended by new constructors or equations. This is just a trick of the
6.7 -presentation. In reality one has to define a new datatype and a new function.}%
6.8 +presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
6.9 +a new datatype and a new function.}%
6.10 \end{isamarkuptext}%
6.11 \isamarkuptrue%
6.12 \isamarkupfalse%
6.13 @@ -178,7 +179,7 @@
6.14 \isamarkupfalse%
6.15 \isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
6.16 \isamarkupfalse%
6.17 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
6.18 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
6.19 \isamarkupfalse%
6.20 \isacommand{done}\isamarkupfalse%
6.21 %
6.22 @@ -229,7 +230,7 @@
6.23 From this proposition the original goal follows easily:%
6.24 \end{isamarkuptxt}%
6.25 \ \isamarkuptrue%
6.26 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
6.27 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}\isamarkupfalse%
6.28 %
6.29 \begin{isamarkuptxt}%
6.30 \noindent
6.31 @@ -275,7 +276,7 @@
6.32 \isa{fast} can prove the base case quickly:%
6.33 \end{isamarkuptxt}%
6.34 \ \isamarkuptrue%
6.35 -\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
6.36 +\isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isamarkupfalse%
6.37 %
6.38 \begin{isamarkuptxt}%
6.39 \noindent
6.40 @@ -375,7 +376,7 @@
6.41 Both are solved automatically:%
6.42 \end{isamarkuptxt}%
6.43 \ \isamarkuptrue%
6.44 -\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
6.45 +\isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
6.46 \isamarkupfalse%
6.47 \isacommand{done}\isamarkupfalse%
6.48 %
7.1 --- a/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 18 17:46:17 2002 +0100
7.2 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 18 18:30:19 2002 +0100
7.3 @@ -58,7 +58,7 @@
7.4 \isamarkupfalse%
7.5 \isacommand{apply}{\isacharparenleft}drule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ case\ i\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ t\ {\isacharbar}\ Suc\ i\ {\isasymRightarrow}\ f\ i{\isachardoublequote}\ \isakeyword{in}\ bspec{\isacharparenright}\isanewline
7.6 \isamarkupfalse%
7.7 -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}Paths{\isacharunderscore}def\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline
7.8 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ Paths{\isacharunderscore}def\ split{\isacharcolon}\ nat{\isachardot}split{\isacharparenright}\isanewline
7.9 \isamarkupfalse%
7.10 \isacommand{done}\isamarkupfalse%
7.11 %
7.12 @@ -133,7 +133,7 @@
7.13 \ \isamarkupfalse%
7.14 \isacommand{apply}{\isacharparenleft}simp\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}\ add{\isacharcolon}\ af{\isacharunderscore}def{\isacharparenright}\isanewline
7.15 \ \isamarkupfalse%
7.16 -\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
7.17 +\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isamarkupfalse%
7.18 %
7.19 \begin{isamarkuptxt}%
7.20 Having proved the main goal, we return to the proof obligation that the
7.21 @@ -149,13 +149,13 @@
7.22 \isamarkuptrue%
7.23 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
7.24 \isamarkupfalse%
7.25 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
7.26 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ wf{\isacharunderscore}iff{\isacharunderscore}no{\isacharunderscore}infinite{\isacharunderscore}down{\isacharunderscore}chain{\isacharparenright}\isanewline
7.27 \isamarkupfalse%
7.28 \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline
7.29 \isamarkupfalse%
7.30 \isacommand{apply}{\isacharparenleft}rule\ ex{\isacharunderscore}infinite{\isacharunderscore}path{\isacharparenright}\isanewline
7.31 \isamarkupfalse%
7.32 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharparenright}\isanewline
7.33 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ Paths{\isacharunderscore}def{\isacharparenright}\isanewline
7.34 \isamarkupfalse%
7.35 \isacommand{done}\isamarkupfalse%
7.36 %
7.37 @@ -177,7 +177,7 @@
7.38 \isamarkuptrue%
7.39 \isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ \ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
7.40 \isamarkupfalse%
7.41 -\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}Avoid{\isachardot}intros{\isacharparenright}\isanewline
7.42 +\isacommand{by}{\isacharparenleft}auto\ elim{\isacharcolon}\ Avoid{\isacharunderscore}in{\isacharunderscore}lfp\ intro{\isacharcolon}\ Avoid{\isachardot}intros{\isacharparenright}\isanewline
7.43 \isanewline
7.44 \isamarkupfalse%
7.45 \isamarkupfalse%
8.1 --- a/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 18 17:46:17 2002 +0100
8.2 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Fri Jan 18 18:30:19 2002 +0100
8.3 @@ -217,7 +217,7 @@
8.4 \isamarkupfalse%
8.5 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
8.6 \isamarkupfalse%
8.7 -\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
8.8 +\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma{\isacharparenright}\isanewline
8.9 \isamarkupfalse%
8.10 \isacommand{done}\isamarkupfalse%
8.11 %
9.1 --- a/doc-src/TutorialI/Inductive/AB.thy Fri Jan 18 17:46:17 2002 +0100
9.2 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri Jan 18 18:30:19 2002 +0100
9.3 @@ -165,7 +165,7 @@
9.4 size[x\<in>take i w @ drop i w. \<not>P x]+2;
9.5 size[x\<in>take i w. P x] = size[x\<in>take i w. \<not>P x]+1\<rbrakk>
9.6 \<Longrightarrow> size[x\<in>drop i w. P x] = size[x\<in>drop i w. \<not>P x]+1"
9.7 -by(simp del:append_take_drop_id)
9.8 +by(simp del: append_take_drop_id)
9.9
9.10 text{*\noindent
9.11 In the proof we have disabled the normally useful lemma
9.12 @@ -280,8 +280,8 @@
9.13 apply(assumption)
9.14 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
9.15 apply(rule S_A_B.intros)
9.16 - apply(force simp add:min_less_iff_disj)
9.17 -by(force simp add:min_less_iff_disj split add: nat_diff_split)
9.18 + apply(force simp add: min_less_iff_disj)
9.19 +by(force simp add: min_less_iff_disj split add: nat_diff_split)
9.20
9.21 text{*
9.22 We conclude this section with a comparison of our proof with
10.1 --- a/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 18 17:46:17 2002 +0100
10.2 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Fri Jan 18 18:30:19 2002 +0100
10.3 @@ -49,7 +49,7 @@
10.4 (*<*)
10.5 apply simp
10.6 apply simp
10.7 -apply(simp add:dvd_def)
10.8 +apply(simp add: dvd_def)
10.9 apply(clarify)
10.10 apply(rule_tac x = "Suc k" in exI)
10.11 apply simp
11.1 --- a/doc-src/TutorialI/Inductive/Star.thy Fri Jan 18 17:46:17 2002 +0100
11.2 +++ b/doc-src/TutorialI/Inductive/Star.thy Fri Jan 18 18:30:19 2002 +0100
11.3 @@ -167,7 +167,7 @@
11.4 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*"
11.5 apply(erule rtc.induct);
11.6 apply blast;
11.7 -apply(blast intro:rtc_step)
11.8 +apply(blast intro: rtc_step)
11.9 done
11.10
11.11 end
12.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex Fri Jan 18 17:46:17 2002 +0100
12.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri Jan 18 18:30:19 2002 +0100
12.3 @@ -182,7 +182,7 @@
12.4 \ \ \ \ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isasymrbrakk}\isanewline
12.5 \ \ \ {\isasymLongrightarrow}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}drop\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline
12.6 \isamarkupfalse%
12.7 -\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse%
12.8 +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isamarkupfalse%
12.9 %
12.10 \begin{isamarkuptext}%
12.11 \noindent
12.12 @@ -325,9 +325,9 @@
12.13 \isamarkupfalse%
12.14 \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline
12.15 \ \isamarkupfalse%
12.16 -\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
12.17 +\isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline
12.18 \isamarkupfalse%
12.19 -\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
12.20 +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}\ min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
12.21 %
12.22 \begin{isamarkuptext}%
12.23 We conclude this section with a comparison of our proof with
13.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 18 17:46:17 2002 +0100
13.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Jan 18 18:30:19 2002 +0100
13.3 @@ -80,8 +80,7 @@
13.4 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
13.5 \end{equation}
13.6 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
13.7 -Now you can perform
13.8 -perform induction on~$x$. An example appears in
13.9 +Now you can perform induction on~$x$. An example appears in
13.10 \S\ref{sec:complete-ind} below.
13.11
13.12 The very same problem may occur in connection with rule induction. Remember
13.13 @@ -264,7 +263,7 @@
13.14 the induction hypothesis:
13.15 *};
13.16 apply(blast);
13.17 -by(blast elim:less_SucE)
13.18 +by(blast elim: less_SucE)
13.19
13.20 text{*\noindent
13.21 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
14.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Jan 18 17:46:17 2002 +0100
14.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Jan 18 18:30:19 2002 +0100
14.3 @@ -92,8 +92,7 @@
14.4 \forall y@1 \dots y@n.~ x = t \longrightarrow C.
14.5 \end{equation}
14.6 where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is a new variable.
14.7 -Now you can perform
14.8 -perform induction on~$x$. An example appears in
14.9 +Now you can perform induction on~$x$. An example appears in
14.10 \S\ref{sec:complete-ind} below.
14.11
14.12 The very same problem may occur in connection with rule induction. Remember
14.13 @@ -309,7 +308,7 @@
14.14 \ \isamarkuptrue%
14.15 \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
14.16 \isamarkupfalse%
14.17 -\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
14.18 +\isacommand{by}{\isacharparenleft}blast\ elim{\isacharcolon}\ less{\isacharunderscore}SucE{\isacharparenright}\isamarkupfalse%
14.19 %
14.20 \begin{isamarkuptext}%
14.21 \noindent
15.1 --- a/doc-src/TutorialI/Overview/Ind.thy Fri Jan 18 17:46:17 2002 +0100
15.2 +++ b/doc-src/TutorialI/Overview/Ind.thy Fri Jan 18 18:30:19 2002 +0100
15.3 @@ -93,7 +93,7 @@
15.4 lemma "wf{(x,y). (x,y) \<in> r \<and> y \<in> acc r}"
15.5 thm wfI
15.6 apply(rule_tac A = "acc r" in wfI)
15.7 - apply (blast elim:acc.elims)
15.8 + apply (blast elim: acc.elims)
15.9 apply(simp(no_asm_use))
15.10 thm acc.induct
15.11 apply(erule acc.induct)
16.1 --- a/doc-src/TutorialI/Overview/Isar.thy Fri Jan 18 17:46:17 2002 +0100
16.2 +++ b/doc-src/TutorialI/Overview/Isar.thy Fri Jan 18 18:30:19 2002 +0100
16.3 @@ -9,7 +9,7 @@
16.4 (is "lfp ?F = ?toA")
16.5 proof
16.6 show "lfp ?F \<subseteq> ?toA"
16.7 - by (blast intro!: lfp_lowerbound intro:rtrancl_trans)
16.8 + by (blast intro!: lfp_lowerbound intro: rtrancl_trans)
16.9
16.10 show "?toA \<subseteq> lfp ?F"
16.11 proof
17.1 --- a/doc-src/TutorialI/Overview/RECDEF.thy Fri Jan 18 17:46:17 2002 +0100
17.2 +++ b/doc-src/TutorialI/Overview/RECDEF.thy Fri Jan 18 18:30:19 2002 +0100
17.3 @@ -73,7 +73,7 @@
17.4
17.5 lemma "mirror(mirror t) = t"
17.6 apply(induct_tac t rule: mirror.induct)
17.7 -apply(simp add:rev_map sym[OF map_compose] cong:map_cong)
17.8 +apply(simp add: rev_map sym[OF map_compose] cong: map_cong)
17.9 done
17.10
17.11 text{*
18.1 --- a/doc-src/TutorialI/Overview/Sets.thy Fri Jan 18 17:46:17 2002 +0100
18.2 +++ b/doc-src/TutorialI/Overview/Sets.thy Fri Jan 18 18:30:19 2002 +0100
18.3 @@ -102,7 +102,7 @@
18.4
18.5 theorem "mc f = {s. s \<Turnstile> f}";
18.6 apply(induct_tac f);
18.7 -apply(auto simp add:EF_lemma);
18.8 +apply(auto simp add: EF_lemma);
18.9 done;
18.10
18.11 text{*
19.1 --- a/doc-src/TutorialI/Protocol/protocol.tex Fri Jan 18 17:46:17 2002 +0100
19.2 +++ b/doc-src/TutorialI/Protocol/protocol.tex Fri Jan 18 18:30:19 2002 +0100
19.3 @@ -324,6 +324,7 @@
19.4 \isa{priK} maps agents to their private keys. It is defined in terms of
19.5 \isa{invKey} and \isa{pubK} by a translation; therefore \isa{priK} is
19.6 not a proper constant, so we declare it using \isacommand{syntax}
19.7 +(cf.\ \S\ref{sec:syntax-translations}).
19.8 \begin{isabelle}
19.9 \isacommand{consts}\ \,pubK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
19.10 \isacommand{syntax}\ priK\ \ \ \ ::\ "agent\ =>\ key"\isanewline
20.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy Fri Jan 18 17:46:17 2002 +0100
20.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Fri Jan 18 18:30:19 2002 +0100
20.3 @@ -19,13 +19,13 @@
20.4 *}
20.5
20.6 lemma "trev(trev t) = t"
20.7 -apply(induct_tac t rule:trev.induct)
20.8 +apply(induct_tac t rule: trev.induct)
20.9 txt{*
20.10 @{subgoals[display,indent=0]}
20.11 Both the base case and the induction step fall to simplification:
20.12 *}
20.13
20.14 -by(simp_all add:rev_map sym[OF map_compose] cong:map_cong)
20.15 +by(simp_all add: rev_map sym[OF map_compose] cong: map_cong)
20.16
20.17 text{*\noindent
20.18 If the proof of the induction step mystifies you, we recommend that you go through
21.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Fri Jan 18 17:46:17 2002 +0100
21.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Fri Jan 18 18:30:19 2002 +0100
21.3 @@ -20,7 +20,7 @@
21.4 \isamarkuptrue%
21.5 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
21.6 \isamarkupfalse%
21.7 -\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
21.8 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}\isamarkupfalse%
21.9 %
21.10 \begin{isamarkuptxt}%
21.11 \begin{isabelle}%
21.12 @@ -32,7 +32,7 @@
21.13 Both the base case and the induction step fall to simplification:%
21.14 \end{isamarkuptxt}%
21.15 \isamarkuptrue%
21.16 -\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
21.17 +\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}\isamarkupfalse%
21.18 %
21.19 \begin{isamarkuptext}%
21.20 \noindent
22.1 --- a/doc-src/TutorialI/Rules/rules.tex Fri Jan 18 17:46:17 2002 +0100
22.2 +++ b/doc-src/TutorialI/Rules/rules.tex Fri Jan 18 18:30:19 2002 +0100
22.3 @@ -1245,7 +1245,7 @@
22.4 ``the greatest divisior of~$n$.''
22.5 It returns an arbitrary value unless the formula has a unique solution.
22.6 An \textbf{indefinite description} formalizes the word ``some,'' as in
22.7 -``some member of~$S$.'' It differs from a definition description in not
22.8 +``some member of~$S$.'' It differs from a definite description in not
22.9 requiring the solution to be unique: it uses the axiom of choice to pick any
22.10 solution.
22.11
23.1 --- a/doc-src/TutorialI/Sets/Examples.thy Fri Jan 18 17:46:17 2002 +0100
23.2 +++ b/doc-src/TutorialI/Sets/Examples.thy Fri Jan 18 18:30:19 2002 +0100
23.3 @@ -90,7 +90,7 @@
23.4 text{*A type constraint lets it work*}
23.5
23.6 text{*An issue here: how do we discuss the distinction between ASCII and
23.7 -X-symbol notation? Here the latter disambiguates.*}
23.8 +symbol notation? Here the latter disambiguates.*}
23.9
23.10
23.11 text{*
24.1 --- a/doc-src/TutorialI/Sets/sets.tex Fri Jan 18 17:46:17 2002 +0100
24.2 +++ b/doc-src/TutorialI/Sets/sets.tex Fri Jan 18 18:30:19 2002 +0100
24.3 @@ -51,7 +51,7 @@
24.4 \end{isabelle}
24.5
24.6 Here are two of the many installed theorems concerning set
24.7 -complement.\index{complement!of a set}%
24.8 +complement.\index{complement!of a set}
24.9 Note that it is denoted by a minus sign.
24.10 \begin{isabelle}
24.11 (c\ \isasymin\ -\ A)\ =\ (c\ \isasymnotin\ A)
24.12 @@ -745,7 +745,7 @@
24.13 The \textbf{reflexive and transitive closure} of the
24.14 relation~\isa{r} is written with a
24.15 postfix syntax. In ASCII we write \isa{r\isacharcircum*} and in
24.16 -X-symbol notation~\isa{r\isactrlsup *}. It is the least solution of the
24.17 +symbol notation~\isa{r\isactrlsup *}. It is the least solution of the
24.18 equation
24.19 \begin{isabelle}
24.20 r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *)
25.1 --- a/doc-src/TutorialI/Types/Axioms.thy Fri Jan 18 17:46:17 2002 +0100
25.2 +++ b/doc-src/TutorialI/Types/Axioms.thy Fri Jan 18 18:30:19 2002 +0100
25.3 @@ -54,7 +54,7 @@
25.4 when the proposition is not a theorem. The proof is easy:
25.5 *}
25.6
25.7 -by(simp add:less_le antisym);
25.8 +by(simp add: less_le antisym);
25.9
25.10 text{* We could now continue in this vein and develop a whole theory of
25.11 results about partial orders. Eventually we will want to apply these results
25.12 @@ -147,7 +147,7 @@
25.13 are easily proved:
25.14 *}
25.15
25.16 - apply(simp_all (no_asm_use) add:less_le);
25.17 + apply(simp_all (no_asm_use) add: less_le);
25.18 apply(blast intro: trans antisym);
25.19 apply(blast intro: refl);
25.20 done
25.21 @@ -161,7 +161,7 @@
25.22 (*
25.23 instance strord < parord
25.24 apply intro_classes;
25.25 -apply(simp_all (no_asm_use) add:le_less);
25.26 +apply(simp_all (no_asm_use) add: le_less);
25.27 apply(blast intro: less_trans);
25.28 apply(erule disjE);
25.29 apply(erule disjE);
25.30 @@ -193,7 +193,7 @@
25.31 \begin{figure}[htbp]
25.32 \[
25.33 \begin{array}{r@ {}r@ {}c@ {}l@ {}l}
25.34 -& & \isa{term}\\
25.35 +& & \isa{type}\\
25.36 & & |\\
25.37 & & \isa{ordrel}\\
25.38 & & |\\
26.1 --- a/doc-src/TutorialI/Types/Overloading1.thy Fri Jan 18 17:46:17 2002 +0100
26.2 +++ b/doc-src/TutorialI/Types/Overloading1.thy Fri Jan 18 18:30:19 2002 +0100
26.3 @@ -5,7 +5,7 @@
26.4 text{*
26.5 We now start with the theory of ordering relations, which we shall phrase
26.6 in terms of the two binary symbols @{text"<<"} and @{text"<<="}
26.7 -to avoid clashes with @{text"<"} and @{text"\<le>"} in theory @{text
26.8 +to avoid clashes with @{text"<"} and @{text"<="} in theory @{text
26.9 Main}. To restrict the application of @{text"<<"} and @{text"<<="} we
26.10 introduce the class @{text ordrel}:
26.11 *}
27.1 --- a/doc-src/TutorialI/Types/Pairs.thy Fri Jan 18 17:46:17 2002 +0100
27.2 +++ b/doc-src/TutorialI/Types/Pairs.thy Fri Jan 18 18:30:19 2002 +0100
27.3 @@ -55,7 +55,7 @@
27.4 *}
27.5
27.6 lemma "(\<lambda>(x,y).x) p = fst p"
27.7 -by(simp add:split_def)
27.8 +by(simp add: split_def)
27.9
27.10 text{* This works well if rewriting with @{thm[source]split_def} finishes the
27.11 proof, as it does above. But if it does not, you end up with exactly what
27.12 @@ -102,7 +102,7 @@
27.13 can be split as above. The same is true for paired set comprehension:
27.14 *}
27.15
27.16 -(*<*)by(simp split:split_split)(*>*)
27.17 +(*<*)by(simp split: split_split)(*>*)
27.18 lemma "p \<in> {(x,y). x=y} \<longrightarrow> fst p = snd p"
27.19 apply simp
27.20
27.21 @@ -114,7 +114,7 @@
27.22 The same proof procedure works for
27.23 *}
27.24
27.25 -(*<*)by(simp split:split_split)(*>*)
27.26 +(*<*)by(simp split: split_split)(*>*)
27.27 lemma "p \<in> {(x,y). x=y} \<Longrightarrow> fst p = snd p"
27.28
27.29 txt{*\noindent
27.30 @@ -125,7 +125,7 @@
27.31 may be present in the goal. Consider the following function:
27.32 *}
27.33
27.34 -(*<*)by(simp split:split_split_asm)(*>*)
27.35 +(*<*)by(simp split: split_split_asm)(*>*)
27.36 consts swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
27.37 primrec
27.38 "swap (x,y) = (y,x)"
27.39 @@ -184,7 +184,7 @@
27.40 (*<*)
27.41 lemma "\<And>p q. swap(swap p) = q \<longrightarrow> p = q"
27.42 (*>*)
27.43 -apply(simp add:split_paired_all)
27.44 +apply(simp add: split_paired_all)
27.45 (*<*)done(*>*)
27.46 text{*\noindent
27.47 Finally, the simplifier automatically splits all @{text"\<forall>"} and
28.1 --- a/doc-src/TutorialI/Types/Typedefs.thy Fri Jan 18 17:46:17 2002 +0100
28.2 +++ b/doc-src/TutorialI/Types/Typedefs.thy Fri Jan 18 18:30:19 2002 +0100
28.3 @@ -195,7 +195,7 @@
28.4
28.5 txt{*\noindent Again this follows easily from a pre-proved general theorem:*}
28.6
28.7 -apply(rule_tac x = x in Abs_three_induct)
28.8 +apply(induct_tac x rule: Abs_three_induct)
28.9
28.10 txt{*
28.11 @{subgoals[display,indent=0]}
29.1 --- a/doc-src/TutorialI/Types/document/Axioms.tex Fri Jan 18 17:46:17 2002 +0100
29.2 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Fri Jan 18 18:30:19 2002 +0100
29.3 @@ -64,7 +64,7 @@
29.4 when the proposition is not a theorem. The proof is easy:%
29.5 \end{isamarkuptxt}%
29.6 \isamarkuptrue%
29.7 -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
29.8 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ less{\isacharunderscore}le\ antisym{\isacharparenright}\isamarkupfalse%
29.9 %
29.10 \begin{isamarkuptext}%
29.11 We could now continue in this vein and develop a whole theory of
29.12 @@ -193,7 +193,7 @@
29.13 are easily proved:%
29.14 \end{isamarkuptxt}%
29.15 \ \ \isamarkuptrue%
29.16 -\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}less{\isacharunderscore}le{\isacharparenright}\isanewline
29.17 +\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ {\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}\ add{\isacharcolon}\ less{\isacharunderscore}le{\isacharparenright}\isanewline
29.18 \ \isamarkupfalse%
29.19 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ trans\ antisym{\isacharparenright}\isanewline
29.20 \isamarkupfalse%
29.21 @@ -232,7 +232,7 @@
29.22 \begin{figure}[htbp]
29.23 \[
29.24 \begin{array}{r@ {}r@ {}c@ {}l@ {}l}
29.25 -& & \isa{term}\\
29.26 +& & \isa{type}\\
29.27 & & |\\
29.28 & & \isa{ordrel}\\
29.29 & & |\\
30.1 --- a/doc-src/TutorialI/Types/document/Overloading1.tex Fri Jan 18 17:46:17 2002 +0100
30.2 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex Fri Jan 18 18:30:19 2002 +0100
30.3 @@ -10,7 +10,7 @@
30.4 \begin{isamarkuptext}%
30.5 We now start with the theory of ordering relations, which we shall phrase
30.6 in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
30.7 -to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
30.8 +to avoid clashes with \isa{{\isacharless}} and \isa{{\isacharless}{\isacharequal}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
30.9 introduce the class \isa{ordrel}:%
30.10 \end{isamarkuptext}%
30.11 \isamarkuptrue%
31.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 18 17:46:17 2002 +0100
31.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Jan 18 18:30:19 2002 +0100
31.3 @@ -67,7 +67,7 @@
31.4 \isamarkuptrue%
31.5 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline
31.6 \isamarkupfalse%
31.7 -\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
31.8 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
31.9 %
31.10 \begin{isamarkuptext}%
31.11 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
31.12 @@ -218,7 +218,7 @@
31.13 \end{isamarkuptext}%
31.14 \isamarkuptrue%
31.15 \isamarkupfalse%
31.16 -\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
31.17 +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
31.18 \isamarkupfalse%
31.19 %
31.20 \begin{isamarkuptext}%
32.1 --- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 18 17:46:17 2002 +0100
32.2 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Jan 18 18:30:19 2002 +0100
32.3 @@ -218,7 +218,7 @@
32.4 \noindent Again this follows easily from a pre-proved general theorem:%
32.5 \end{isamarkuptxt}%
32.6 \isamarkuptrue%
32.7 -\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
32.8 +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ rule{\isacharcolon}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
32.9 %
32.10 \begin{isamarkuptxt}%
32.11 \begin{isabelle}%