bang_args;
authorwenzelm
Mon Oct 15 20:32:13 2001 +0200 (2001-10-15)
changeset 11775e7eeca372b7c
parent 11774 3bc4f67d7fe1
child 11776 d4f9de0bde28
bang_args;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Oct 15 20:31:52 2001 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Oct 15 20:32:13 2001 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
     1.5    val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
     1.6    val no_args: 'a attribute -> Args.src -> 'a attribute
     1.7 +  val bang_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
     1.8    val add_del_args: 'a attribute -> 'a attribute -> Args.src -> 'a attribute
     1.9    val setup: (theory -> theory) list
    1.10  end;
    1.11 @@ -156,6 +157,9 @@
    1.12  
    1.13  fun no_args x = syntax (Scan.succeed x);
    1.14  
    1.15 +fun bang_args a b x = syntax
    1.16 +  (Scan.lift Args.bang >> K a || Scan.succeed b) x;
    1.17 +
    1.18  fun add_del_args add del x = syntax
    1.19    (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x;
    1.20