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 "ML_file" :: thy_load % "ML" |
17 and "SML_file" "ML_file" :: thy_load % "ML" |
18 and "header" :: diag |
18 and "header" :: diag |
19 and "chapter" :: thy_heading1 |
19 and "chapter" :: thy_heading1 |
20 and "section" :: thy_heading2 |
20 and "section" :: thy_heading2 |
21 and "subsection" :: thy_heading3 |
21 and "subsection" :: thy_heading3 |
22 and "subsubsection" :: thy_heading4 |
22 and "subsubsection" :: thy_heading4 |