tuned args;
authorwenzelm
Tue Sep 19 23:53:00 2000 +0200 (2000-09-19 ago)
changeset 100344bca6b2d2589
parent 10033 fc4e7432b2b1
child 10035 c095955e7575
tuned args;
src/Provers/classical.ML
src/Provers/simplifier.ML
src/Provers/splitter.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
     1.1 --- a/src/Provers/classical.ML	Tue Sep 19 23:52:37 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Sep 19 23:53:00 2000 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  *)
     1.5  
     1.6  (*higher precedence than := facilitates use of references*)
     1.7 -infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
     1.8 +infix 4 addSIs addSEs addSDs addIs addEs addDs addXIs addXEs addXDs delrules
     1.9    addSWrapper delSWrapper addWrapper delWrapper
    1.10    addSbefore addSaltern addbefore addaltern
    1.11    addD2 addE2 addSD2 addSE2;
    1.12 @@ -56,6 +56,9 @@
    1.13    val addSDs            : claset * thm list -> claset
    1.14    val addSEs            : claset * thm list -> claset
    1.15    val addSIs            : claset * thm list -> claset
    1.16 +  val addXDs            : claset * thm list -> claset
    1.17 +  val addXEs            : claset * thm list -> claset
    1.18 +  val addXIs            : claset * thm list -> claset
    1.19    val delrules          : claset * thm list -> claset
    1.20    val addSWrapper       : claset * (string * wrapper) -> claset
    1.21    val delSWrapper       : claset *  string            -> claset
    1.22 @@ -514,8 +517,6 @@
    1.23          dup_netpair  = dup_netpair}
    1.24    end;
    1.25  
    1.26 -infix 4 addXIs addXEs addXDs;
    1.27 -
    1.28  val op addXIs = rev_foldl addXI;
    1.29  val op addXEs = rev_foldl addXE;
    1.30  
    1.31 @@ -1028,18 +1029,12 @@
    1.32  val destN = "dest";
    1.33  val ruleN = "rule";
    1.34  
    1.35 -val colon = Args.$$$ ":";
    1.36 -val query = Args.$$$ "?";
    1.37 -val bang = Args.$$$ "!";
    1.38 -val query_colon = Args.$$$ "?:";
    1.39 -val bang_colon = Args.$$$ "!:";
    1.40 -
    1.41  fun cla_att change xtra haz safe = Attrib.syntax
    1.42 -  (Scan.lift ((query >> K xtra || bang >> K safe || Scan.succeed haz) >> change));
    1.43 +  (Scan.lift ((Args.query >> K xtra || Args.bang >> K safe || Scan.succeed haz) >> change));
    1.44  
    1.45  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
    1.46  
    1.47 -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
    1.48 +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
    1.49  val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
    1.50  
    1.51  
    1.52 @@ -1149,16 +1144,16 @@
    1.53  (* automatic methods *)
    1.54  
    1.55  val cla_modifiers =
    1.56 - [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
    1.57 -  Args.$$$ destN -- bang_colon >> K (I, safe_dest_local),
    1.58 -  Args.$$$ destN -- colon >> K (I, haz_dest_local),
    1.59 -  Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
    1.60 -  Args.$$$ elimN -- bang_colon >> K (I, safe_elim_local),
    1.61 -  Args.$$$ elimN -- colon >> K (I, haz_elim_local),
    1.62 -  Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
    1.63 -  Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
    1.64 -  Args.$$$ introN -- colon >> K (I, haz_intro_local),
    1.65 -  Args.$$$ Args.delN -- colon >> K (I, rule_del_local)];
    1.66 + [Args.$$$ destN -- Args.query_colon >> K ((I, xtra_dest_local):Method.modifier),
    1.67 +  Args.$$$ destN -- Args.bang_colon >> K (I, safe_dest_local),
    1.68 +  Args.$$$ destN -- Args.colon >> K (I, haz_dest_local),
    1.69 +  Args.$$$ elimN -- Args.query_colon >> K (I, xtra_elim_local),
    1.70 +  Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim_local),
    1.71 +  Args.$$$ elimN -- Args.colon >> K (I, haz_elim_local),
    1.72 +  Args.$$$ introN -- Args.query_colon >> K (I, xtra_intro_local),
    1.73 +  Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro_local),
    1.74 +  Args.$$$ introN -- Args.colon >> K (I, haz_intro_local),
    1.75 +  Args.del -- Args.colon >> K (I, rule_del_local)];
    1.76  
    1.77  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    1.78    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
     2.1 --- a/src/Provers/simplifier.ML	Tue Sep 19 23:52:37 2000 +0200
     2.2 +++ b/src/Provers/simplifier.ML	Tue Sep 19 23:53:00 2000 +0200
     2.3 @@ -518,19 +518,19 @@
     2.4  
     2.5  val cong_modifiers =
     2.6   [Args.$$$ congN -- Args.colon >> K ((I, cong_add_local):Method.modifier),
     2.7 -  Args.$$$ congN -- Args.$$$ Args.addN -- Args.colon >> K (I, cong_add_local),
     2.8 -  Args.$$$ congN -- Args.$$$ Args.delN -- Args.colon >> K (I, cong_del_local)];
     2.9 +  Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add_local),
    2.10 +  Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del_local)];
    2.11  
    2.12  val simp_modifiers =
    2.13   [Args.$$$ simpN -- Args.colon >> K (I, simp_add_local),
    2.14 -  Args.$$$ simpN -- Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
    2.15 -  Args.$$$ simpN -- Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
    2.16 +  Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add_local),
    2.17 +  Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del_local),
    2.18    Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    2.19     @ cong_modifiers;
    2.20  
    2.21  val simp_modifiers' =
    2.22 - [Args.$$$ Args.addN -- Args.colon >> K (I, simp_add_local),
    2.23 -  Args.$$$ Args.delN -- Args.colon >> K (I, simp_del_local),
    2.24 + [Args.add -- Args.colon >> K (I, simp_add_local),
    2.25 +  Args.del -- Args.colon >> K (I, simp_del_local),
    2.26    Args.$$$ onlyN -- Args.colon >> K (map_local_simpset clear_ss, simp_add_local)]
    2.27     @ cong_modifiers;
    2.28  
     3.1 --- a/src/Provers/splitter.ML	Tue Sep 19 23:52:37 2000 +0200
     3.2 +++ b/src/Provers/splitter.ML	Tue Sep 19 23:53:00 2000 +0200
     3.3 @@ -417,8 +417,8 @@
     3.4  
     3.5  val split_modifiers =
     3.6   [Args.$$$ splitN -- Args.colon >> K ((I, split_add_local): Method.modifier),
     3.7 -  Args.$$$ splitN -- Args.$$$ Args.addN -- Args.colon >> K (I, split_add_local),
     3.8 -  Args.$$$ splitN -- Args.$$$ Args.delN -- Args.colon >> K (I, split_del_local)];
     3.9 +  Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add_local),
    3.10 +  Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del_local)];
    3.11  
    3.12  val split_args = #2 oo Method.syntax (Args.mode "asm" -- Attrib.local_thms);
    3.13  
     4.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 19 23:52:37 2000 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 19 23:53:00 2000 +0200
     4.3 @@ -156,8 +156,8 @@
     4.4  
     4.5  fun no_args x = syntax (Scan.succeed x);
     4.6  
     4.7 -fun add_del_args add del x = syntax (Scan.lift
     4.8 -    (Args.$$$ Args.addN >> K add || Args.$$$ Args.delN >> K del || Scan.succeed add)) x;
     4.9 +fun add_del_args add del x = syntax
    4.10 +  (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x;
    4.11  
    4.12  
    4.13  
     5.1 --- a/src/Pure/Isar/method.ML	Tue Sep 19 23:52:37 2000 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Tue Sep 19 23:53:00 2000 +0200
     5.3 @@ -202,7 +202,7 @@
     5.4  val intro_local = mk_att LocalRules.map add_intro;
     5.5  val rule_del_local = mk_att LocalRules.map del_rule;
     5.6  
     5.7 -fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ Args.delN) >> K att);
     5.8 +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att);
     5.9  
    5.10  end;
    5.11