fixed section syntax;
authorwenzelm
Wed Mar 08 23:47:44 2000 +0100 (2000-03-08)
changeset 838252d5fae273dd
parent 8381 4fc7e63781f6
child 8383 2dd4823c744f
fixed section syntax;
src/Provers/classical.ML
src/Provers/simplifier.ML
     1.1 --- a/src/Provers/classical.ML	Wed Mar 08 23:46:59 2000 +0100
     1.2 +++ b/src/Provers/classical.ML	Wed Mar 08 23:47:44 2000 +0100
     1.3 @@ -1021,8 +1021,11 @@
     1.4  val delN = "del";
     1.5  val delruleN = "delrule";
     1.6  
     1.7 +val colon = Args.$$$ ":";
     1.8  val query = Args.$$$ "?";
     1.9  val qquery = Args.$$$ "??";
    1.10 +val query_colon = Args.$$$ "?:";
    1.11 +val qquery_colon = Args.$$$ "??:";
    1.12  
    1.13  fun cla_att change xtra haz safe = Attrib.syntax
    1.14    (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
    1.15 @@ -1133,16 +1136,16 @@
    1.16  (* automatic methods *)
    1.17  
    1.18  val cla_modifiers =
    1.19 - [Args.$$$ destN -- qquery >> K ((I, xtra_dest_local):Method.modifier),
    1.20 -  Args.$$$ destN -- query >> K (I, haz_dest_local),
    1.21 -  Args.$$$ destN >> K (I, safe_dest_local),
    1.22 -  Args.$$$ elimN -- qquery >> K (I, xtra_elim_local),
    1.23 -  Args.$$$ elimN -- query >> K (I, haz_elim_local),
    1.24 -  Args.$$$ elimN >> K (I, safe_elim_local),
    1.25 -  Args.$$$ introN -- qquery >> K (I, xtra_intro_local),
    1.26 -  Args.$$$ introN -- query >> K (I, haz_intro_local),
    1.27 -  Args.$$$ introN >> K (I, safe_intro_local),
    1.28 -  Args.$$$ delN >> K (I, delrule_local)];
    1.29 + [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier),
    1.30 +  Args.$$$ destN -- query_colon >> K (I, haz_dest_local),
    1.31 +  Args.$$$ destN -- colon >> K (I, safe_dest_local),
    1.32 +  Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local),
    1.33 +  Args.$$$ elimN -- query_colon >> K (I, haz_elim_local),
    1.34 +  Args.$$$ elimN -- colon >> K (I, safe_elim_local),
    1.35 +  Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local),
    1.36 +  Args.$$$ introN -- query_colon >> K (I, haz_intro_local),
    1.37 +  Args.$$$ introN -- colon >> K (I, safe_intro_local),
    1.38 +  Args.$$$ delN -- colon >> K (I, delrule_local)];
    1.39  
    1.40  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    1.41    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
     2.1 --- a/src/Provers/simplifier.ML	Wed Mar 08 23:46:59 2000 +0100
     2.2 +++ b/src/Provers/simplifier.ML	Wed Mar 08 23:47:44 2000 +0100
     2.3 @@ -474,17 +474,19 @@
     2.4  
     2.5  (* simplification *)
     2.6  
     2.7 +val colon = Args.$$$ ":";
     2.8 +
     2.9  val simp_modifiers =
    2.10 - [Args.$$$ simpN -- Args.$$$ addN >> K (I, simp_add_local),
    2.11 -  Args.$$$ simpN -- Args.$$$ delN >> K (I, simp_del_local),
    2.12 -  Args.$$$ simpN -- Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
    2.13 -  Args.$$$ otherN >> K (I, I)];
    2.14 + [Args.$$$ simpN -- Args.$$$ addN -- colon >> K (I, simp_add_local),
    2.15 +  Args.$$$ simpN -- Args.$$$ delN -- colon >> K (I, simp_del_local),
    2.16 +  Args.$$$ simpN -- Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
    2.17 +  Args.$$$ otherN -- colon >> K (I, I)];
    2.18  
    2.19  val simp_modifiers' =
    2.20 - [Args.$$$ addN >> K (I, simp_add_local),
    2.21 -  Args.$$$ delN >> K (I, simp_del_local),
    2.22 -  Args.$$$ onlyN >> K (map_local_simpset clear_ss, simp_add_local),
    2.23 -  Args.$$$ otherN >> K (I, I)];
    2.24 + [Args.$$$ addN -- colon >> K (I, simp_add_local),
    2.25 +  Args.$$$ delN -- colon >> K (I, simp_del_local),
    2.26 +  Args.$$$ onlyN -- colon >> K (map_local_simpset clear_ss, simp_add_local),
    2.27 +  Args.$$$ otherN -- colon >> K (I, I)];
    2.28  
    2.29  fun simp_method tac =
    2.30    (fn prems => fn ctxt => Method.METHOD (fn facts =>