equal
deleted
inserted
replaced
1064 Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo |
1064 Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo |
1065 prepare_free_constructors Plugin_Name.make_filter Syntax.read_term; |
1065 prepare_free_constructors Plugin_Name.make_filter Syntax.read_term; |
1066 |
1066 |
1067 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term; |
1067 val parse_bound_term = Parse.binding --| @{keyword ":"} -- Parse.term; |
1068 |
1068 |
1069 type ctr_options = (string -> bool) * bool; |
1069 type ctr_options = Plugin_Name.filter * bool; |
1070 type ctr_options_cmd = (Proof.context -> string -> bool) * bool; |
1070 type ctr_options_cmd = (Proof.context -> Plugin_Name.filter) * bool; |
1071 |
1071 |
1072 val default_ctr_options : ctr_options = (K true, false); |
1072 val default_ctr_options : ctr_options = (Plugin_Name.default_filter, false); |
1073 val default_ctr_options_cmd : ctr_options_cmd = (K (K true), false); |
1073 val default_ctr_options_cmd : ctr_options_cmd = (K Plugin_Name.default_filter, false); |
1074 |
1074 |
1075 val parse_ctr_options = |
1075 val parse_ctr_options = |
1076 Scan.optional (@{keyword "("} |-- Parse.list1 |
1076 Scan.optional (@{keyword "("} |-- Parse.list1 |
1077 (Plugin_Name.parse_filter >> (apfst o K) || |
1077 (Plugin_Name.parse_filter >> (apfst o K) || |
1078 Parse.reserved "discs_sels" >> (apsnd o K o K true)) --| |
1078 Parse.reserved "discs_sels" >> (apsnd o K o K true)) --| |