equal
deleted
inserted
replaced
64 "Record full proof objects internally" |
64 "Record full proof objects internally" |
65 end |
65 end |
66 |
66 |
67 val thm_deps_pref = |
67 val thm_deps_pref = |
68 let |
68 let |
69 fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN) |
69 fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) |
70 fun set s = if PgipTypes.read_pgipbool s then |
70 fun set s = if PgipTypes.read_pgipbool s then |
71 change print_mode (insert (op =) thm_depsN) |
71 change print_mode (insert (op =) thm_depsN) |
72 else |
72 else |
73 change print_mode (remove (op =) thm_depsN) |
73 change print_mode (remove (op =) thm_depsN) |
74 in |
74 in |