# HG changeset patch
# User wenzelm
# Date 1412711081 -7200
# Node ID 4b41df5fef811e43a74f4286c4188fdcc52bc0bf
# Parent  782f0b662caec441204534882557bc9642964cab
clarified whitespace;

diff -r 782f0b662cae -r 4b41df5fef81 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Tue Oct 07 21:29:59 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Tue Oct 07 21:44:41 2014 +0200
@@ -940,19 +940,19 @@
   \end{description}
 \<close>
 
-  method_setup my_method1 = \<open>
-    Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
-\<close>  "my first method (without any arguments)"
+  method_setup my_method1 =
+    \<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close>
+    "my first method (without any arguments)"
 
-  method_setup my_method2 = \<open>
-    Scan.succeed (fn ctxt: Proof.context =>
-      SIMPLE_METHOD' (fn i: int => no_tac))
-\<close>  "my second method (with context)"
+  method_setup my_method2 =
+    \<open>Scan.succeed (fn ctxt: Proof.context =>
+      SIMPLE_METHOD' (fn i: int => no_tac))\<close>
+    "my second method (with context)"
 
-  method_setup my_method3 = \<open>
-    Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
-      SIMPLE_METHOD' (fn i: int => no_tac))
-\<close>  "my third method (with theorem arguments and context)"
+  method_setup my_method3 =
+    \<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
+      SIMPLE_METHOD' (fn i: int => no_tac))\<close>
+    "my third method (with theorem arguments and context)"
 
 
 section \<open>Generalized elimination \label{sec:obtain}\<close>
diff -r 782f0b662cae -r 4b41df5fef81 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Tue Oct 07 21:29:59 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Oct 07 21:44:41 2014 +0200
@@ -1110,15 +1110,15 @@
   \end{description}
 \<close>
 
-  attribute_setup my_rule = \<open>
-    Attrib.thms >> (fn ths =>
+  attribute_setup my_rule =
+    \<open>Attrib.thms >> (fn ths =>
       Thm.rule_attribute
         (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths
           in th' end))\<close>
 
-  attribute_setup my_declaration = \<open>
-    Attrib.thms >> (fn ths =>
+  attribute_setup my_declaration =
+    \<open>Attrib.thms >> (fn ths =>
       Thm.declaration_attribute
         (fn th: thm => fn context: Context.generic =>
           let val context' = context