/[mojave]/metaprl/editor/ml/mp.ml
ViewVC logotype

Diff of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2574 by jyh, Mon Jan 25 18:34:13 1999 UTC revision 2604 by lolorigo, Thu Mar 4 15:02:04 1999 UTC
# Line 101  Line 101 
101   * Nuprl5 interface.   * Nuprl5 interface.
102   *)   *)
103  let edit_list_modules = edit_list_modules  let edit_list_modules = edit_list_modules
104    let edit_list_module_all = edit_list_module_all
105  let edit_list_module = edit_list_module  let edit_list_module = edit_list_module
106    let edit_list_module_rw = edit_list_module_rw
107  let edit_list_parents = edit_list_parents  let edit_list_parents = edit_list_parents
108  let edit_list_dforms = edit_list_dforms  let edit_list_dforms = edit_list_dforms
109  let edit_list_precs = edit_list_precs  let edit_list_precs = edit_list_precs
110  let edit_list_prec_rels = edit_list_prec_rels  let edit_list_prec_rels = edit_list_prec_rels
111  let edit_create_thm = edit_create_thm  let edit_create_thm = edit_create_thm
112    let edit_create_rw = edit_create_rw
113  let edit_cd_thm = edit_cd_thm  let edit_cd_thm = edit_cd_thm
114  let edit_set_goal = edit_set_goal  let edit_set_goal = edit_set_goal
115  let edit_set_redex = edit_set_redex  let edit_set_redex = edit_set_redex
# Line 115  Line 118 
118  let edit_set_params = edit_set_params  let edit_set_params = edit_set_params
119  let edit_refine = edit_refine  let edit_refine = edit_refine
120  let edit_node = edit_node  let edit_node = edit_node
121    let edit_save = edit_save
122  let edit_undo = edit_undo  let edit_undo = edit_undo
123    
124  let _ = Shell.main ()  let _ = Shell.main ()

Legend:
Removed from v.2574  
changed lines
  Added in v.2604

  ViewVC Help
Powered by ViewVC 1.1.26