equal
deleted
inserted
replaced
30 end |
30 end |
31 |
31 |
32 structure ProofDisplay: PROOF_DISPLAY = |
32 structure ProofDisplay: PROOF_DISPLAY = |
33 struct |
33 struct |
34 |
34 |
35 (* ML toplevel pretty printing *) |
35 (* toplevel pretty printing *) |
36 |
36 |
37 val debug = ref false; |
37 val debug = ref false; |
38 |
38 |
39 fun pprint_context ctxt = Pretty.pprint |
39 fun pprint_context ctxt = Pretty.pprint |
40 (if ! debug then |
40 (if ! debug then |
45 |
45 |
46 val pprint_typ = pprint ProofContext.pretty_typ; |
46 val pprint_typ = pprint ProofContext.pretty_typ; |
47 val pprint_term = pprint ProofContext.pretty_term; |
47 val pprint_term = pprint ProofContext.pretty_term; |
48 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT); |
48 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT); |
49 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct); |
49 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct); |
50 fun pprint_thm th = pprint ProofContext.pretty_thm (Thm.theory_of_thm th) th; |
50 val pprint_thm = Pretty.pprint o ProofContext.legacy_pretty_thm true; |
51 |
51 |
52 |
52 |
53 (* theorems and theory *) |
53 (* theorems and theory *) |
54 |
54 |
55 fun pretty_theorems_diff prev_thms thy = |
55 fun pretty_theorems_diff prev_thms thy = |