# HG changeset patch
# User wenzelm
# Date 1135347665 -3600
# Node ID 9b8b33098ced3bf7aacf20554a86ec00598dbde3
# Parent  96260fb114493b2fe5b977342a919ed90eda4cd1
tuned;

diff -r 96260fb11449 -r 9b8b33098ced NEWS
--- a/NEWS	Fri Dec 23 15:18:13 2005 +0100
+++ b/NEWS	Fri Dec 23 15:21:05 2005 +0100
@@ -169,13 +169,13 @@
 needs to be structured carefully as a two-level conjunction, using
 lists of propositions separated by 'and':
 
-lemma
-  shows "a : A ==> P1 a"
-        "a : A ==> P2 a"
-    and "b : B ==> Q1 b"
-        "b : B ==> Q2 b"
-        "b : B ==> Q3 b"
-proof (induct set: A B)
+  lemma
+    shows "a : A ==> P1 a"
+          "a : A ==> P2 a"
+      and "b : B ==> Q1 b"
+          "b : B ==> Q2 b"
+          "b : B ==> Q3 b"
+  proof (induct set: A B)
 
 * Provers/induct: support coinduction as well.  See
 src/HOL/Library/Coinductive_List.thy for various examples.