src/Doc/Tutorial/Recdef/Induction.thy
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
     1.1 --- a/src/Doc/Tutorial/Recdef/Induction.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Recdef/Induction.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*<*)
     1.5 -theory Induction imports examples simplification begin;
     1.6 +theory Induction imports examples simplification begin
     1.7  (*>*)
     1.8  
     1.9  text{*
    1.10 @@ -19,7 +19,7 @@
    1.11  involving the predefined @{term"map"} functional on lists:
    1.12  *}
    1.13  
    1.14 -lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
    1.15 +lemma "map f (sep(x,xs)) = sep(f x, map f xs)"
    1.16  
    1.17  txt{*\noindent
    1.18  Note that @{term"map f xs"}
    1.19 @@ -27,7 +27,7 @@
    1.20  this lemma by recursion induction over @{term"sep"}:
    1.21  *}
    1.22  
    1.23 -apply(induct_tac x xs rule: sep.induct);
    1.24 +apply(induct_tac x xs rule: sep.induct)
    1.25  
    1.26  txt{*\noindent
    1.27  The resulting proof state has three subgoals corresponding to the three
    1.28 @@ -36,7 +36,7 @@
    1.29  The rest is pure simplification:
    1.30  *}
    1.31  
    1.32 -apply simp_all;
    1.33 +apply simp_all
    1.34  done
    1.35  
    1.36  text{*