equal
deleted
inserted
replaced
67 let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p |
67 let fun proof_tr [p, P] = Const (@{const_syntax Proof}, dummyT) $ P $ p |
68 in [(@{syntax_const "_Proof"}, proof_tr)] end |
68 in [(@{syntax_const "_Proof"}, proof_tr)] end |
69 *} |
69 *} |
70 |
70 |
71 (*show_proofs = true displays the proof terms -- they are ENORMOUS*) |
71 (*show_proofs = true displays the proof terms -- they are ENORMOUS*) |
72 ML {* val (show_proofs, setup_show_proofs) = Attrib.config_bool "show_proofs" (K false) *} |
72 ML {* val show_proofs = Attrib.setup_config_bool @{binding show_proofs} (K false) *} |
73 setup setup_show_proofs |
|
74 |
73 |
75 print_translation (advanced) {* |
74 print_translation (advanced) {* |
76 let |
75 let |
77 fun proof_tr' ctxt [P, p] = |
76 fun proof_tr' ctxt [P, p] = |
78 if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P |
77 if Config.get ctxt show_proofs then Const (@{syntax_const "_Proof"}, dummyT) $ p $ P |