Args.addN, Args.delN;
authorwenzelm
Wed Sep 13 22:31:19 2000 +0200 (2000-09-13 ago)
changeset 995224914e42b857
parent 9951 5610c4acb48d
child 9953 035a8288310a
Args.addN, Args.delN;
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Provers/splitter.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Provers/clasimp.ML	Wed Sep 13 22:29:37 2000 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Wed Sep 13 22:31:19 2000 +0200
     1.3 @@ -272,13 +272,11 @@
     1.4  (* method modifiers *)
     1.5  
     1.6  val iffN = "iff";
     1.7 -val addN = "add";
     1.8 -val delN = "del";
     1.9  
    1.10  val iff_modifiers =
    1.11   [Args.$$$ iffN -- Args.colon >> K ((I, iff_add_local): Method.modifier),
    1.12 -  Args.$$$ iffN -- Args.$$$ addN -- Args.colon >> K (I, iff_add_local),
    1.13 -  Args.$$$ iffN -- Args.$$$ delN -- Args.colon >> K (I, iff_del_local)];
    1.14 +  Args.$$$ iffN -- Args.$$$ Args.addN -- Args.colon >> K (I, iff_add_local),
    1.15 +  Args.$$$ iffN -- Args.$$$ Args.delN -- Args.colon >> K (I, iff_del_local)];
    1.16  
    1.17  val clasimp_modifiers =
    1.18    Simplifier.simp_modifiers @ Splitter.split_modifiers @
     2.1 --- a/src/Provers/classical.ML	Wed Sep 13 22:29:37 2000 +0200
     2.2 +++ b/src/Provers/classical.ML	Wed Sep 13 22:31:19 2000 +0200
     2.3 @@ -1027,7 +1027,6 @@
     2.4  val elimN = "elim";
     2.5  val destN = "dest";
     2.6  val ruleN = "rule";
     2.7 -val delN = "del";
     2.8  
     2.9  val colon = Args.$$$ ":";
    2.10  val query = Args.$$$ "?";
    2.11 @@ -1040,7 +1039,7 @@
    2.12  
    2.13  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
    2.14  
    2.15 -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att);
    2.16 +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
    2.17  val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
    2.18  
    2.19  
    2.20 @@ -1159,7 +1158,7 @@
    2.21    Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
    2.22    Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
    2.23    Args.$$$ introN -- colon >> K (I, haz_intro_local),
    2.24 -  Args.$$$ delN -- colon >> K (I, rule_del_local)];
    2.25 +  Args.$$$ Args.delN -- colon >> K (I, rule_del_local)];
    2.26  
    2.27  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    2.28    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
     3.1 --- a/src/Provers/simplifier.ML	Wed Sep 13 22:29:37 2000 +0200
     3.2 +++ b/src/Provers/simplifier.ML	Wed Sep 13 22:31:19 2000 +0200
     3.3 @@ -460,8 +460,6 @@
     3.4  
     3.5  val simpN = "simp";
     3.6  val congN = "cong";
     3.7 -val addN = "add";
     3.8 -val delN = "del";
     3.9  val onlyN = "only";
    3.10  val no_asmN = "no_asm";
    3.11  val no_asm_useN = "no_asm_use";
    3.12 @@ -518,19 +516,19 @@
    3.13  
    3.14  val cong_modifiers =
    3.15   [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
    3.16 -  Args.$$$ congN -- Args.$$$ addN -- Args.colon >> K (I, cong_add_local),
    3.17 -  Args.$$$ congN -- Args.$$$ delN -- Args.colon >> K (I, cong_del_local)];
    3.18 +  Args.$$$ congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
    3.19 +  Args.$$$ congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local)];
    3.20  
    3.21  val simp_modifiers =
    3.22   [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
    3.23 -  Args.$$$ simpN -- Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
    3.24 -  Args.$$$ simpN -- Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
    3.25 +  Args.$$$ simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
    3.26 +  Args.$$$ simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
    3.27    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    3.28     @ cong_modifiers;
    3.29  
    3.30  val simp_modifiers' =
    3.31 - [Args.$$$ addN -- Args.colon >> K (I, simp_add_local),
    3.32 -  Args.$$$ delN -- Args.colon >> K (I, simp_del_local),
    3.33 + [Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
    3.34 +  Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
    3.35    Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    3.36     @ cong_modifiers;
    3.37  
     4.1 --- a/src/Provers/splitter.ML	Wed Sep 13 22:29:37 2000 +0200
     4.2 +++ b/src/Provers/splitter.ML	Wed Sep 13 22:31:19 2000 +0200
     4.3 @@ -417,8 +417,8 @@
     4.4  
     4.5  val split_modifiers =
     4.6   [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
     4.7 -  Args.$$$ splitN -- Args.$$$ "add" -- Args.colon >> K (I, split_add_local),
     4.8 -  Args.$$$ splitN -- Args.$$$ "del" -- Args.colon >> K (I, split_del_local)];
     4.9 +  Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local),
    4.10 +  Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)];
    4.11  
    4.12  val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
    4.13  
     5.1 --- a/src/Pure/Isar/args.ML	Wed Sep 13 22:29:37 2000 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Wed Sep 13 22:31:19 2000 +0200
     5.3 @@ -29,6 +29,8 @@
     5.4    val nat: T list -> int * T list
     5.5    val int: T list -> int * T list
     5.6    val var: T list -> indexname * T list
     5.7 +  val addN: string
     5.8 +  val delN: string
     5.9    val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    5.10    val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    5.11    val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
    5.12 @@ -135,6 +137,9 @@
    5.13  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
    5.14  val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
    5.15  
    5.16 +val addN = "add";
    5.17 +val delN = "del";
    5.18 +
    5.19  
    5.20  (* enumerations *)
    5.21  
     6.1 --- a/src/Pure/Isar/attrib.ML	Wed Sep 13 22:29:37 2000 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Wed Sep 13 22:31:19 2000 +0200
     6.3 @@ -156,8 +156,8 @@
     6.4  
     6.5  fun no_args x = syntax (Scan.succeed x);
     6.6  
     6.7 -fun add_del_args add del x =
     6.8 -  syntax (Scan.lift (Args.$$$ "add" >> K add || Args.$$$ "del" >> K del || Scan.succeed add)) x;
     6.9 +fun add_del_args add del x = syntax (Scan.lift
    6.10 +    (Args.$$$ Args.addN >> K add || Args.$$$ Args.delN >> K del || Scan.succeed add)) x;
    6.11  
    6.12  
    6.13  
     7.1 --- a/src/Pure/Isar/method.ML	Wed Sep 13 22:29:37 2000 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Wed Sep 13 22:31:19 2000 +0200
     7.3 @@ -199,7 +199,7 @@
     7.4  val intro_local = mk_att LocalRules.map add_intro;
     7.5  val rule_del_local = mk_att LocalRules.map del_rule;
     7.6  
     7.7 -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ "del") >> K att);
     7.8 +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
     7.9  
    7.10  end;
    7.11