# HG changeset patch
# User wenzelm
# Date 969400380 -7200
# Node ID 4bca6b2d258939034934790048f51a74281cdbcb
# Parent  fc4e7432b2b124141809406b5dc10158aee83aae
tuned args;

diff -r fc4e7432b2b1 -r 4bca6b2d2589 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Provers/classical.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -15,7 +15,7 @@
 *)
 
 (*higher precedence than := facilitates use of references*)
-infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
+infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules
   addSWrapper delSWrapper addWrapper delWrapper
   addSbefore addSaltern addbefore addaltern
   addD2 addE2 addSD2 addSE2;
@@ -56,6 +56,9 @@
   val addSDs            : claset * thm list -> claset
   val addSEs            : claset * thm list -> claset
   val addSIs            : claset * thm list -> claset
+  val addXDs            : claset * thm list -> claset
+  val addXEs            : claset * thm list -> claset
+  val addXIs            : claset * thm list -> claset
   val delrules          : claset * thm list -> claset
   val addSWrapper       : claset * (string * wrapper) -> claset
   val delSWrapper       : claset *  string            -> claset
@@ -514,8 +517,6 @@
         dup_netpair  = dup_netpair}
   end;
 
-infix 4 addXIs addXEs addXDs;
-
 val op addXIs = rev_foldl addXI;
 val op addXEs = rev_foldl addXE;
 
@@ -1028,18 +1029,12 @@
 val destN = "dest";
 val ruleN = "rule";
 
-val colon = Args.$$$ ":";
-val query = Args.$$$ "?";
-val bang = Args.$$$ "!";
-val query_colon = Args.$$$ "?:";
-val bang_colon = Args.$$$ "!:";
-
 fun cla_att change xtra haz safe = Attrib.syntax
-  (Scan.lift ((query >> K xtra || bang >> K safe || Scan.succeed haz) >> change));
+  (Scan.lift ((Args.query >> K xtra || Args.bang >> K safe || Scan.succeed haz) >> change));
 
 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
 
-fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
+fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
 val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
 
 
@@ -1149,16 +1144,16 @@
 (* automatic methods *)
 
 val cla_modifiers =
- [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
-  Args.$$$ destN -- bang_colon >> K (I, safe_dest_local),
-  Args.$$$ destN -- colon >> K (I, haz_dest_local),
-  Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
-  Args.$$$ elimN -- bang_colon >> K (I, safe_elim_local),
-  Args.$$$ elimN -- colon >> K (I, haz_elim_local),
-  Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
-  Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
-  Args.$$$ introN -- colon >> K (I, haz_intro_local),
-  Args.$$$ Args.delN -- colon >> K (I, rule_del_local)];
+ [Args.$$$ destN -- Args.query_colon >> K ((I, xtra_dest_local):Method.modifier),
+  Args.$$$ destN -- Args.bang_colon >> K (I, safe_dest_local),
+  Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
+  Args.$$$ elimN -- Args.query_colon >> K (I, xtra_elim_local),
+  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
+  Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
+  Args.$$$ introN -- Args.query_colon >> K (I, xtra_intro_local),
+  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
+  Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
+  Args.del -- Args.colon >> K (I, rule_del_local)];
 
 fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
   ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
diff -r fc4e7432b2b1 -r 4bca6b2d2589 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Provers/simplifier.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -518,19 +518,19 @@
 
 val cong_modifiers =
  [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
-  Args.$$$ congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
-  Args.$$$ congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local)];
+  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
+  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
 
 val simp_modifiers =
  [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
+  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 
 val simp_modifiers' =
- [Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
-  Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
+ [Args.add -- Args.colon >> K (I, simp_add_local),
+  Args.del -- Args.colon >> K (I, simp_del_local),
   Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    @ cong_modifiers;
 
diff -r fc4e7432b2b1 -r 4bca6b2d2589 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Provers/splitter.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -417,8 +417,8 @@
 
 val split_modifiers =
  [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
-  Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local),
-  Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)];
+  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
+  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
 
 val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
 
diff -r fc4e7432b2b1 -r 4bca6b2d2589 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -156,8 +156,8 @@
 
 fun no_args x = syntax (Scan.succeed x);
 
-fun add_del_args add del x = syntax (Scan.lift
-    (Args.$$$ Args.addN >> K add || Args.$$$ Args.delN >> K del || Scan.succeed add)) x;
+fun add_del_args add del x = syntax
+  (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x;
 
 
 
diff -r fc4e7432b2b1 -r 4bca6b2d2589 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Sep 19 23:52:37 2000 +0200
+++ b/src/Pure/Isar/method.ML	Tue Sep 19 23:53:00 2000 +0200
@@ -202,7 +202,7 @@
 val intro_local = mk_att LocalRules.map add_intro;
 val rule_del_local = mk_att LocalRules.map del_rule;
 
-fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
+fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
 
 end;