equal
deleted
inserted
replaced
52 end) |
52 end) |
53 ); |
53 ); |
54 |
54 |
55 fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans; |
55 fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans; |
56 |
56 |
57 val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterSyntax.Keyword.diag refute_parser; |
57 val refute_cmd = OuterSyntax.improper_command "refute" "try to find a model that refutes a given subgoal" OuterKeyword.diag refute_parser; |
58 |
58 |
59 (* ------------------------------------------------------------------------- *) |
59 (* ------------------------------------------------------------------------- *) |
60 (* set up the 'refute_params' command *) |
60 (* set up the 'refute_params' command *) |
61 (* ------------------------------------------------------------------------- *) |
61 (* ------------------------------------------------------------------------- *) |
62 |
62 |
88 end) |
88 end) |
89 end; |
89 end; |
90 |
90 |
91 fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans; |
91 fun refute_params_parser tokens = (refute_params_scan_args tokens) |>> refute_params_trans; |
92 |
92 |
93 val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterSyntax.Keyword.thy_decl refute_params_parser; |
93 val refute_params_cmd = OuterSyntax.command "refute_params" "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl refute_params_parser; |
94 |
94 |
95 end; |
95 end; |
96 |
96 |
97 (* ------------------------------------------------------------------------- *) |
97 (* ------------------------------------------------------------------------- *) |
98 (* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's *) |
98 (* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's *) |