equal
deleted
inserted
replaced
6 ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr"] *} |
6 ML {* no_document use_thys ["Efficient_Nat", "Code_Char_chr"] *} |
7 |
7 |
8 ML_val {* Code_Target.code_width := 74 *} |
8 ML_val {* Code_Target.code_width := 74 *} |
9 |
9 |
10 ML {* |
10 ML {* |
11 fun pr_class ctxt = Sign.extern_class (ProofContext.theory_of ctxt) |
11 fun pr_class ctxt = enclose "\\isa{" "}" o Sign.extern_class (ProofContext.theory_of ctxt) |
12 o Sign.read_class (ProofContext.theory_of ctxt); |
12 o Sign.read_class (ProofContext.theory_of ctxt); |
13 *} |
13 *} |
14 |
14 |
15 ML {* |
15 ML {* |
16 val _ = ThyOutput.add_commands |
16 val _ = ThyOutput.add_commands |