1019 val elimN = "elim"; |
1019 val elimN = "elim"; |
1020 val destN = "dest"; |
1020 val destN = "dest"; |
1021 val delN = "del"; |
1021 val delN = "del"; |
1022 val delruleN = "delrule"; |
1022 val delruleN = "delrule"; |
1023 |
1023 |
|
1024 val colon = Args.$$$ ":"; |
1024 val query = Args.$$$ "?"; |
1025 val query = Args.$$$ "?"; |
1025 val qquery = Args.$$$ "??"; |
1026 val qquery = Args.$$$ "??"; |
|
1027 val query_colon = Args.$$$ "?:"; |
|
1028 val qquery_colon = Args.$$$ "??:"; |
1026 |
1029 |
1027 fun cla_att change xtra haz safe = Attrib.syntax |
1030 fun cla_att change xtra haz safe = Attrib.syntax |
1028 (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change)); |
1031 (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change)); |
1029 |
1032 |
1030 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); |
1033 fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); |
1131 |
1134 |
1132 |
1135 |
1133 (* automatic methods *) |
1136 (* automatic methods *) |
1134 |
1137 |
1135 val cla_modifiers = |
1138 val cla_modifiers = |
1136 [Args.$$$ destN -- qquery >> K ((I, xtra_dest_local):Method.modifier), |
1139 [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier), |
1137 Args.$$$ destN -- query >> K (I, haz_dest_local), |
1140 Args.$$$ destN -- query_colon >> K (I, haz_dest_local), |
1138 Args.$$$ destN >> K (I, safe_dest_local), |
1141 Args.$$$ destN -- colon >> K (I, safe_dest_local), |
1139 Args.$$$ elimN -- qquery >> K (I, xtra_elim_local), |
1142 Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local), |
1140 Args.$$$ elimN -- query >> K (I, haz_elim_local), |
1143 Args.$$$ elimN -- query_colon >> K (I, haz_elim_local), |
1141 Args.$$$ elimN >> K (I, safe_elim_local), |
1144 Args.$$$ elimN -- colon >> K (I, safe_elim_local), |
1142 Args.$$$ introN -- qquery >> K (I, xtra_intro_local), |
1145 Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local), |
1143 Args.$$$ introN -- query >> K (I, haz_intro_local), |
1146 Args.$$$ introN -- query_colon >> K (I, haz_intro_local), |
1144 Args.$$$ introN >> K (I, safe_intro_local), |
1147 Args.$$$ introN -- colon >> K (I, safe_intro_local), |
1145 Args.$$$ delN >> K (I, delrule_local)]; |
1148 Args.$$$ delN -- colon >> K (I, delrule_local)]; |
1146 |
1149 |
1147 fun cla_meth tac prems ctxt = Method.METHOD (fn facts => |
1150 fun cla_meth tac prems ctxt = Method.METHOD (fn facts => |
1148 ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); |
1151 ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); |
1149 |
1152 |
1150 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => |
1153 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => |