module displays. import lj, html. type display_tactic (goal -> goal -> o) -> o. type text goal -> goal -> o. type html goal -> goal -> o. type html_init goal -> goal -> o. type see goal -> goal -> o. display_tactic see. display_tactic text. display_tactic html. display_tactic html_init. see In In :- term_to_string In Str, print "Internal form of sequent:\n", print Str, print "\n". text In In :- write_seq In. html G G :- html_seq G. html_init G G :- html_open_out "seq.html" (ooo "\ \Display of sequents\n\ \\n\n" ).