# HG changeset patch
# User wenzelm
# Date 1498468068 -7200
# Node ID 8d34d42c40cb7d85c39a127ec13aaa404462ea33
# Parent  d91108ba94747cc4de4c857a8ed720b9098adc22
clarified indentation;

diff -r d91108ba9474 -r 8d34d42c40cb src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Jun 24 21:23:48 2017 +0200
+++ b/src/Pure/Pure.thy	Mon Jun 26 11:07:48 2017 +0200
@@ -7,11 +7,11 @@
 theory Pure
 keywords
     "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
-    "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
-    "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
+    "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+    "overloaded" "pervasive" "premises" "structure" "unchecked"
   and "private" "qualified" :: before_command
-  and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
-    "obtains" "shows" "where" "|" :: quasi_command
+  and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
+    "obtains" "shows" "when" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl