equal
deleted
inserted
replaced
1186 (** outer syntax **) |
1186 (** outer syntax **) |
1187 |
1187 |
1188 val print_clasetP = |
1188 val print_clasetP = |
1189 OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
1189 OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
1190 OuterSyntax.Keyword.diag |
1190 OuterSyntax.Keyword.diag |
1191 (Scan.succeed (Toplevel.keep |
1191 (Scan.succeed (Toplevel.no_timing o (Toplevel.keep |
1192 (Toplevel.node_case print_claset (print_local_claset o Proof.context_of)))); |
1192 (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))))); |
1193 |
1193 |
1194 val _ = OuterSyntax.add_parsers [print_clasetP]; |
1194 val _ = OuterSyntax.add_parsers [print_clasetP]; |
1195 |
1195 |
1196 |
1196 |
1197 end; |
1197 end; |