src/Pure/Pure.thy
changeset 58868 c5e1cce7ace3
parent 58860 fee7cfa69c50
child 58918 8d36bc5eaed3
     1.1 --- a/src/Pure/Pure.thy	Sun Nov 02 13:26:20 2014 +0100
     1.2 +++ b/src/Pure/Pure.thy	Sun Nov 02 15:27:37 2014 +0100
     1.3 @@ -14,15 +14,12 @@
     1.4      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     1.5      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
     1.6    and "theory" :: thy_begin % "theory"
     1.7 -  and "header" :: diag
     1.8 -  and "chapter" :: thy_heading1
     1.9 -  and "section" :: thy_heading2
    1.10 -  and "subsection" :: thy_heading3
    1.11 -  and "subsubsection" :: thy_heading4
    1.12 +  and "header" :: heading
    1.13 +  and "chapter" :: heading
    1.14 +  and "section" :: heading
    1.15 +  and "subsection" :: heading
    1.16 +  and "subsubsection" :: heading
    1.17    and "text" "text_raw" :: thy_decl
    1.18 -  and "sect" :: prf_heading2 % "proof"
    1.19 -  and "subsect" :: prf_heading3 % "proof"
    1.20 -  and "subsubsect" :: prf_heading4 % "proof"
    1.21    and "txt" "txt_raw" :: prf_decl % "proof"
    1.22    and "default_sort" :: thy_decl == ""
    1.23    and "typedecl" "type_synonym" "nonterminal" "judgment"