src/Pure/Thy/thy_parse.ML
changeset 4952 addfa29d0481
parent 4852 58b5006d36cc
child 4965 06914837e073
equal deleted inserted replaced
4951:8637b29e6c38 4952:addfa29d0481
   544 fun section name pretxt parse =
   544 fun section name pretxt parse =
   545   axm_section name pretxt (parse >> rpair []);
   545   axm_section name pretxt (parse >> rpair []);
   546 
   546 
   547 
   547 
   548 val pure_keywords =
   548 val pure_keywords =
   549  ["end", "ML", "MLtext", "mixfix", "infixr", "infixl", "binder", "global",
   549  ["end", "ML", "mixfix", "infixr", "infixl", "binder", "output", "=",
   550   "local", "output", "=", "+", ",", "<", "{", "}", "(", ")", "[", "]",
   550   "+", ",", "<", "{", "}", "(", ")", "[", "]", "::", "==", "=>",
   551   "::", "==", "=>", "<="];
   551   "<="];
   552 
   552 
   553 val pure_sections =
   553 val pure_sections =
   554  [section "classes" "|> Theory.add_classes" class_decls,
   554  [section "classes" "|> Theory.add_classes" class_decls,
   555   section "default" "|> Theory.add_defsort" sort,
   555   section "default" "|> Theory.add_defsort" sort,
   556   section "types" "" type_decls,
   556   section "types" "" type_decls,