397 ("term", args Args.local_term (output_with pretty_term)), |
397 ("term", args Args.local_term (output_with pretty_term)), |
398 ("term_style", args ((Scan.lift (Args.name || Args.symbol)) -- Args.local_term) (output_with pretty_term_style)), |
398 ("term_style", args ((Scan.lift (Args.name || Args.symbol)) -- Args.local_term) (output_with pretty_term_style)), |
399 ("term_type", args Args.local_term (output_with pretty_term_typ)), |
399 ("term_type", args Args.local_term (output_with pretty_term_typ)), |
400 ("typeof", args Args.local_term (output_with pretty_term_typeof)), |
400 ("typeof", args Args.local_term (output_with pretty_term_typeof)), |
401 ("const", args Args.local_term (output_with pretty_term_const)), |
401 ("const", args Args.local_term (output_with pretty_term_const)), |
402 ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)), |
402 ("typ", args Args.local_typ_abbrev (output_with ProofContext.pretty_typ)), |
403 ("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
403 ("text", args (Scan.lift Args.name) (output_with (K pretty_text))), |
404 ("goals", output_goals true), |
404 ("goals", output_goals true), |
405 ("subgoals", output_goals false), |
405 ("subgoals", output_goals false), |
406 ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
406 ("prf", args Attrib.local_thmss (output_with (pretty_prf false))), |
407 ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))), |
407 ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true))), |