80 basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
80 basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> |
81 basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
81 basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #> |
82 basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #> |
82 basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #> |
83 basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
83 basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #> |
84 basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #> |
84 basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #> |
85 basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory #> |
85 basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #> |
86 basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
86 basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #> |
87 basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #> |
87 basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #> |
88 Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) |
88 Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) |
89 (fn {context = ctxt, source = src, argument = arg} => |
89 (fn {context = ctxt, source = src, argument = arg} => |
90 Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg))); |
90 Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg))); |