src/Doc/Tutorial/Fun/fun0.thy
changeset 58860 fee7cfa69c50
parent 58620 7435b6a3f72e
child 62392 747d36865c2c
     1.1 --- a/src/Doc/Tutorial/Fun/fun0.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Fun/fun0.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     1.5  "sep a []     = []" |
     1.6  "sep a [x]    = [x]" |
     1.7 -"sep a (x#y#zs) = x # a # sep a (y#zs)";
     1.8 +"sep a (x#y#zs) = x # a # sep a (y#zs)"
     1.9  
    1.10  text{*\noindent
    1.11  This time the length of the list decreases with the
    1.12 @@ -217,7 +217,7 @@
    1.13  this lemma by recursion induction over @{term"sep"}:
    1.14  *}
    1.15  
    1.16 -apply(induct_tac x xs rule: sep.induct);
    1.17 +apply(induct_tac x xs rule: sep.induct)
    1.18  
    1.19  txt{*\noindent
    1.20  The resulting proof state has three subgoals corresponding to the three
    1.21 @@ -226,7 +226,7 @@
    1.22  The rest is pure simplification:
    1.23  *}
    1.24  
    1.25 -apply simp_all;
    1.26 +apply simp_all
    1.27  done
    1.28  
    1.29  text{*\noindent The proof goes smoothly because the induction rule