src/HOL/Tools/refute_isar.ML
changeset 26000 b629b4f2026c
parent 24867 e5b55d7be9bb
child 26931 aa226d8405a8
equal deleted inserted replaced
25999:f8bcd311d501 26000:b629b4f2026c
    17 (* ------------------------------------------------------------------------- *)
    17 (* ------------------------------------------------------------------------- *)
    18 (* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    18 (* both 'refute' and 'refute_params' take an optional list of arguments of   *)
    19 (* the form [name1=value1, name2=value2, ...]                                *)
    19 (* the form [name1=value1, name2=value2, ...]                                *)
    20 (* ------------------------------------------------------------------------- *)
    20 (* ------------------------------------------------------------------------- *)
    21 
    21 
    22 	fun repeatd delim scan = scan -- Scan.repeat (OuterParse.$$$ delim |-- scan)
       
    23 		>> op :: || Scan.succeed [];
       
    24 
       
    25 	val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
    22 	val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
    26 
    23 
    27 	val scan_parms = Scan.option
    24 	val scan_parms = Scan.option
    28 		(OuterParse.$$$ "[" |-- (repeatd "," scan_parm) --| OuterParse.$$$ "]");
    25 		(OuterParse.$$$ "[" |-- (OuterParse.list scan_parm) --| OuterParse.$$$ "]");
    29 
    26 
    30 (* ------------------------------------------------------------------------- *)
    27 (* ------------------------------------------------------------------------- *)
    31 (* set up the 'refute' command                                               *)
    28 (* set up the 'refute' command                                               *)
    32 (* ------------------------------------------------------------------------- *)
    29 (* ------------------------------------------------------------------------- *)
    33 
    30