/[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 2494 by jyh, Tue Oct 13 01:14:08 1998 UTC revision 2574 by jyh, Mon Jan 25 18:34:13 1999 UTC
# Line 108  Line 108 
108  let edit_list_prec_rels = edit_list_prec_rels  let edit_list_prec_rels = edit_list_prec_rels
109  let edit_create_thm = edit_create_thm  let edit_create_thm = edit_create_thm
110  let edit_cd_thm = edit_cd_thm  let edit_cd_thm = edit_cd_thm
111    let edit_set_goal = edit_set_goal
112    let edit_set_redex = edit_set_redex
113    let edit_set_contractum = edit_set_contractum
114    let edit_set_assumptions = edit_set_assumptions
115    let edit_set_params = edit_set_params
116  let edit_refine = edit_refine  let edit_refine = edit_refine
117  let edit_node = edit_node  let edit_node = edit_node
118  let edit_undo = edit_undo  let edit_undo = edit_undo

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

  ViewVC Help
Powered by ViewVC 1.1.26