added name_facts;
authorwenzelm
Tue Sep 13 22:19:43 2005 +0200 (2005-09-13)
changeset 173585746c9bd4356
parent 17357 ee2bdca144c7
child 17359 543735c6f424
added name_facts;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Sep 13 22:19:42 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Sep 13 22:19:43 2005 +0200
     1.3 @@ -73,6 +73,8 @@
     1.4    val spec_opt_name: token list -> ((bstring * string) * Attrib.src list) * token list
     1.5    val xthm: token list -> (thmref * Attrib.src list) * token list
     1.6    val xthms1: token list -> (thmref * Attrib.src list) list * token list
     1.7 +  val name_facts: token list ->
     1.8 +    ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
     1.9    val locale_target: token list -> xstring * token list
    1.10    val opt_locale_target: token list -> xstring option * token list
    1.11    val locale_expr: token list -> Locale.expr * token list
    1.12 @@ -314,6 +316,8 @@
    1.13  val xthm = (xname -- thm_sel >> NameSelection || xname >> Name) -- opt_attribs;
    1.14  val xthms1 = Scan.repeat1 xthm;
    1.15  
    1.16 +val name_facts = and_list1 (opt_thm_name "=" -- xthms1);
    1.17 +
    1.18  
    1.19  (* locale elements *)
    1.20