4 Final stage of bootstrapping Pure, based on implicit background theory. |
4 Final stage of bootstrapping Pure, based on implicit background theory. |
5 *) |
5 *) |
6 |
6 |
7 theory Pure |
7 theory Pure |
8 keywords |
8 keywords |
9 "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "==" |
9 "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<equiv>" |
10 "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" |
10 "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>" |
11 "\<rightleftharpoons>" "\<subseteq>" "]" "and" "assumes" |
11 "\<subseteq>" "]" "assumes" "attach" "binder" "constrains" |
12 "attach" "begin" "binder" "constrains" "defines" "fixes" "for" |
12 "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix" |
13 "identifier" "if" "imports" "in" "includes" "infix" "infixl" |
13 "infixl" "infixr" "is" "notes" "obtains" "open" "output" |
14 "infixr" "is" "keywords" "notes" "obtains" "open" "output" |
|
15 "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" |
14 "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" |
16 and "header" :: heading |
|
17 and "chapter" :: heading |
|
18 and "section" :: heading |
|
19 and "subsection" :: heading |
|
20 and "subsubsection" :: heading |
|
21 and "text" "text_raw" :: thy_decl |
15 and "text" "text_raw" :: thy_decl |
22 and "txt" "txt_raw" :: prf_decl % "proof" |
16 and "txt" "txt_raw" :: prf_decl % "proof" |
23 and "default_sort" :: thy_decl == "" |
17 and "default_sort" :: thy_decl == "" |
24 and "typedecl" "type_synonym" "nonterminal" "judgment" |
18 and "typedecl" "type_synonym" "nonterminal" "judgment" |
25 "consts" "syntax" "no_syntax" "translations" "no_translations" "defs" |
19 "consts" "syntax" "no_syntax" "translations" "no_translations" "defs" |