# HG changeset patch
# User wenzelm
# Date 1307016684 -7200
# Node ID 3ba51a3acff01335fce082022aa7b70608bd0320
# Parent  91e229959d4ce5da5897af75001c873ea568c7eb
tuned headings;

diff -r 91e229959d4c -r 3ba51a3acff0 doc-src/IsarRef/Thy/Synopsis.thy
--- a/doc-src/IsarRef/Thy/Synopsis.thy	Thu Jun 02 14:08:46 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy	Thu Jun 02 14:11:24 2011 +0200
@@ -363,7 +363,7 @@
 end
 
 
-section {* Structured induction proofs *}
+section {* Induction *}
 
 subsection {* Induction as Natural Deduction *}
 
@@ -561,7 +561,7 @@
 end
 
 
-section {* Structured Natural Deduction \label{sec:natural-deduction-synopsis} *}
+section {* Natural Deduction \label{sec:natural-deduction-synopsis} *}
 
 subsection {* Rule statements *}
 
diff -r 91e229959d4c -r 3ba51a3acff0 doc-src/IsarRef/Thy/document/Synopsis.tex
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Thu Jun 02 14:08:46 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Thu Jun 02 14:11:24 2011 +0200
@@ -843,7 +843,7 @@
 \isanewline
 \isacommand{end}\isamarkupfalse%
 %
-\isamarkupsection{Structured induction proofs%
+\isamarkupsection{Induction%
 }
 \isamarkuptrue%
 %
@@ -1273,7 +1273,7 @@
 \endisadelimproof
 \isacommand{end}\isamarkupfalse%
 %
-\isamarkupsection{Structured Natural Deduction \label{sec:natural-deduction-synopsis}%
+\isamarkupsection{Natural Deduction \label{sec:natural-deduction-synopsis}%
 }
 \isamarkuptrue%
 %