# HG changeset patch # User wenzelm # Date 1468263480 -7200 # Node ID c4c587aedee8fb906afc62c2e4376069584da711 # Parent afd657fffdf94a7eedcd0173d26cf84c94def2da clarified indentation; diff -r afd657fffdf9 -r c4c587aedee8 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Jul 11 20:37:28 2016 +0200 +++ b/src/Pure/Pure.thy Mon Jul 11 20:58:00 2016 +0200 @@ -8,11 +8,10 @@ keywords "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is" - "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" - "where" "when" "|" + "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites" - "obtains" "shows" :: quasi_command + "obtains" "shows" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl == ""