--- 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));
--- 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;
--- 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);
--- 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;
--- 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;