equal
deleted
inserted
replaced
26 end; |
26 end; |
27 |
27 |
28 signature DISPLAY = |
28 signature DISPLAY = |
29 sig |
29 sig |
30 include BASIC_DISPLAY |
30 include BASIC_DISPLAY |
31 val raw_string_of_sort: sort -> string |
|
32 val raw_string_of_typ: typ -> string |
|
33 val raw_string_of_term: term -> string |
|
34 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
31 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T |
35 val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T |
32 val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T |
36 val pretty_thm: thm -> Pretty.T |
33 val pretty_thm: thm -> Pretty.T |
37 val pretty_thms: thm list -> Pretty.T |
34 val pretty_thms: thm list -> Pretty.T |
38 val pretty_thm_sg: theory -> thm -> Pretty.T |
35 val pretty_thm_sg: theory -> thm -> Pretty.T |
45 val print_goals: int -> thm -> unit |
42 val print_goals: int -> thm -> unit |
46 end; |
43 end; |
47 |
44 |
48 structure Display: DISPLAY = |
45 structure Display: DISPLAY = |
49 struct |
46 struct |
50 |
|
51 (** raw output **) |
|
52 |
|
53 val raw_string_of_sort = Sign.string_of_sort ProtoPure.thy; |
|
54 val raw_string_of_typ = Sign.string_of_typ ProtoPure.thy; |
|
55 val raw_string_of_term = Sign.string_of_term ProtoPure.thy; |
|
56 |
|
57 |
47 |
58 |
48 |
59 (** print thm **) |
49 (** print thm **) |
60 |
50 |
61 val goals_limit = ref 10; (*max number of goals to print*) |
51 val goals_limit = ref 10; (*max number of goals to print*) |