333 |
333 |
334 val _ = add_commands |
334 val _ = add_commands |
335 [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)), |
335 [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)), |
336 ("prop", args Args.local_prop (output_with pretty_term)), |
336 ("prop", args Args.local_prop (output_with pretty_term)), |
337 ("term", args Args.local_term (output_with pretty_term)), |
337 ("term", args Args.local_term (output_with pretty_term)), |
338 ("typ", args Args.local_typ_no_norm (output_with ProofContext.pretty_typ)), |
338 ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)), |
339 ("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
339 ("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
340 ("goals", output_goals true), |
340 ("goals", output_goals true), |
341 ("subgoals", output_goals false), |
341 ("subgoals", output_goals false), |
342 ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
342 ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
343 ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))]; |
343 ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))]; |