src/Pure/Isar/spec_parse.ML
changeset 27816 0dfed2f2822a
parent 27378 0968c0d0b969
child 28083 103d9282a946
equal deleted inserted replaced
27815:2d36632bc5de 27816:0dfed2f2822a
    48 type token = P.token;
    48 type token = P.token;
    49 
    49 
    50 
    50 
    51 (* theorem specifications *)
    51 (* theorem specifications *)
    52 
    52 
    53 val attrib = P.position ((P.keyword_sid || P.xname) -- P.!!! P.arguments) >> Args.src;
    53 val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
    54 val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    54 val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
    55 val opt_attribs = Scan.optional attribs [];
    55 val opt_attribs = Scan.optional attribs [];
    56 
    56 
    57 fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
    57 fun thm_name s = P.name -- opt_attribs --| P.$$$ s;
    58 fun opt_thm_name s =
    58 fun opt_thm_name s =
    62 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    62 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    63 
    63 
    64 val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    64 val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    65 val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    65 val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
    66 
    66 
    67 val thm_sel = P.$$$ "(" |-- P.list1
       
    68  (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
       
    69   P.nat --| P.minus >> Facts.From ||
       
    70   P.nat >> Facts.Single) --| P.$$$ ")";
       
    71 
       
    72 val xthm =
    67 val xthm =
    73   P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    68   P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
    74   (P.alt_string >> Facts.Fact ||
    69   (P.alt_string >> Facts.Fact ||
    75     P.position P.xname -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
    70     P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    76 
    71 
    77 val xthms1 = Scan.repeat1 xthm;
    72 val xthms1 = Scan.repeat1 xthm;
    78 
    73 
    79 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    74 val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    80 
    75