equal
deleted
inserted
replaced
268 "exit" |
268 "exit" |
269 "init_toplevel" |
269 "init_toplevel" |
270 "kill" |
270 "kill" |
271 "kill_thy" |
271 "kill_thy" |
272 "linear_undo" |
272 "linear_undo" |
|
273 "pretty_setmargin" |
273 "quit" |
274 "quit" |
274 "remove_thy" |
275 "remove_thy" |
275 "undo" |
276 "undo" |
276 "undos_proof" |
277 "undos_proof" |
277 "use_thy")) |
278 "use_thy")) |
287 "full_prf" |
288 "full_prf" |
288 "header" |
289 "header" |
289 "help" |
290 "help" |
290 "locale_deps" |
291 "locale_deps" |
291 "pr" |
292 "pr" |
292 "pretty_setmargin" |
|
293 "prf" |
293 "prf" |
294 "print_abbrevs" |
294 "print_abbrevs" |
295 "print_antiquotations" |
295 "print_antiquotations" |
296 "print_attributes" |
296 "print_attributes" |
297 "print_binds" |
297 "print_binds" |