src/Pure/Pure.thy
changeset 56618 874bdedb2313
parent 56275 600f432ab556
child 56797 32963b43a538
     1.1 --- a/src/Pure/Pure.thy	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Pure/Pure.thy	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -14,7 +14,6 @@
     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 "SML_file" "ML_file" :: thy_load % "ML"
     1.8    and "header" :: diag
     1.9    and "chapter" :: thy_heading1
    1.10    and "section" :: thy_heading2
    1.11 @@ -30,6 +29,8 @@
    1.12      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    1.13      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    1.14      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    1.15 +  and "SML_file" "ML_file" :: thy_load % "ML"
    1.16 +  and "SML_import" "SML_export" :: thy_decl % "ML"
    1.17    and "ML" :: thy_decl % "ML"
    1.18    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    1.19    and "ML_val" "ML_command" :: diag % "ML"