equal
deleted
inserted
replaced
12 "attach" "begin" "binder" "constrains" "defines" "fixes" "for" |
12 "attach" "begin" "binder" "constrains" "defines" "fixes" "for" |
13 "identifier" "if" "imports" "in" "includes" "infix" "infixl" |
13 "identifier" "if" "imports" "in" "includes" "infix" "infixl" |
14 "infixr" "is" "keywords" "notes" "obtains" "open" "output" |
14 "infixr" "is" "keywords" "notes" "obtains" "open" "output" |
15 "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" |
15 "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|" |
16 and "theory" :: thy_begin % "theory" |
16 and "theory" :: thy_begin % "theory" |
17 and "SML_file" "ML_file" :: thy_load % "ML" |
|
18 and "header" :: diag |
17 and "header" :: diag |
19 and "chapter" :: thy_heading1 |
18 and "chapter" :: thy_heading1 |
20 and "section" :: thy_heading2 |
19 and "section" :: thy_heading2 |
21 and "subsection" :: thy_heading3 |
20 and "subsection" :: thy_heading3 |
22 and "subsubsection" :: thy_heading4 |
21 and "subsubsection" :: thy_heading4 |
28 and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment" |
27 and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment" |
29 "consts" "syntax" "no_syntax" "translations" "no_translations" "defs" |
28 "consts" "syntax" "no_syntax" "translations" "no_translations" "defs" |
30 "definition" "abbreviation" "type_notation" "no_type_notation" "notation" |
29 "definition" "abbreviation" "type_notation" "no_type_notation" "notation" |
31 "no_notation" "axiomatization" "theorems" "lemmas" "declare" |
30 "no_notation" "axiomatization" "theorems" "lemmas" "declare" |
32 "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl |
31 "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl |
|
32 and "SML_file" "ML_file" :: thy_load % "ML" |
|
33 and "SML_import" "SML_export" :: thy_decl % "ML" |
33 and "ML" :: thy_decl % "ML" |
34 and "ML" :: thy_decl % "ML" |
34 and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) |
35 and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) |
35 and "ML_val" "ML_command" :: diag % "ML" |
36 and "ML_val" "ML_command" :: diag % "ML" |
36 and "simproc_setup" :: thy_decl % "ML" == "" |
37 and "simproc_setup" :: thy_decl % "ML" == "" |
37 and "setup" "local_setup" "attribute_setup" "method_setup" |
38 and "setup" "local_setup" "attribute_setup" "method_setup" |