equal
deleted
inserted
replaced
27 |
27 |
28 (* class antiquotation *) |
28 (* class antiquotation *) |
29 |
29 |
30 local |
30 local |
31 |
31 |
32 fun pr_class ctxt = enclose "\\isa{" "}" o Sign.extern_class (ProofContext.theory_of ctxt) |
32 fun pr_class ctxt = enclose "\\isa{" "}" o Pretty.output o Pretty.str |
33 o Sign.read_class (ProofContext.theory_of ctxt); |
33 o Sign.extern_class (ProofContext.theory_of ctxt) o Sign.read_class (ProofContext.theory_of ctxt); |
34 |
34 |
35 in |
35 in |
36 |
36 |
37 val _ = O.add_commands |
37 val _ = O.add_commands |
38 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))] |
38 [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class))] |