4 The Pure theory, with definitions of Isar commands and some lemmas. |
4 The Pure theory, with definitions of Isar commands and some lemmas. |
5 *) |
5 *) |
6 |
6 |
7 theory Pure |
7 theory Pure |
8 keywords |
8 keywords |
9 "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" |
9 "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>" |
10 "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>" |
10 "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is" |
11 "\<subseteq>" "]" "assumes" "attach" "binder" "constrains" |
11 "open" "output" "overloaded" "pervasive" "premises" "private" "qualified" |
12 "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix" |
12 "structure" "unchecked" "where" "when" "|" |
13 "infixl" "infixr" "is" "notes" "obtains" "open" "output" |
13 and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites" |
14 "overloaded" "pervasive" "premises" "private" "qualified" "rewrites" |
14 "obtains" "shows" :: quasi_command |
15 "shows" "structure" "unchecked" "where" "when" "|" |
|
16 and "text" "txt" :: document_body |
15 and "text" "txt" :: document_body |
17 and "text_raw" :: document_raw |
16 and "text_raw" :: document_raw |
18 and "default_sort" :: thy_decl == "" |
17 and "default_sort" :: thy_decl == "" |
19 and "typedecl" "type_synonym" "nonterminal" "judgment" |
18 and "typedecl" "type_synonym" "nonterminal" "judgment" |
20 "consts" "syntax" "no_syntax" "translations" "no_translations" |
19 "consts" "syntax" "no_syntax" "translations" "no_translations" |