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

Annotation of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2494 - (hide annotations) (download)
Tue Oct 13 01:14:08 1998 UTC (22 years, 9 months ago) by jyh
File size: 2992 byte(s)
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.

1 jyh 2494 (*
2     * This is the main file for MetaPRL.
3     *
4     * ----------------------------------------------------------------
5     *
6     * This file is part of MetaPRL, a modular, higher order
7     * logical framework that provides a logical programming
8     * environment for OCaml and other languages.
9     *
10     * See the file doc/index.html for information on Nuprl,
11     * OCaml, and more information about this system.
12     *
13     * Copyright (C) 1998 Jason Hickey, Cornell University
14     *
15     * This program is free software; you can redistribute it and/or
16     * modify it under the terms of the GNU General Public License
17     * as published by the Free Software Foundation; either version 2
18     * of the License, or (at your option) any later version.
19     *
20     * This program is distributed in the hope that it will be useful,
21     * but WITHOUT ANY WARRANTY; without even the implied warranty of
22     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23     * GNU General Public License for more details.
24     *
25     * You should have received a copy of the GNU General Public License
26     * along with this program; if not, write to the Free Software
27     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28     *
29     * Author: Jason Hickey
30     * jyh@cs.cornell.edu
31     *)
32    
33     module Shell = Shell.Shell (Shell_p4.ShellP4)
34    
35     open Shell
36    
37     (*
38     * Navigation and display.
39     *)
40     let cd = cd
41     let pwd = pwd
42     let set_window_width = set_window_width
43    
44     (*
45     * Module commands.
46     *)
47     let load = load
48     let create_pkg = create_pkg
49     let set_writeable = set_writeable
50     let save = save
51     let save_all = save_all
52    
53     (*
54     * The possible objects in a package.
55     *)
56     let create_rw = create_rw
57     let create_axiom = create_axiom
58     let create_thm = create_thm
59     let create_tptp = create_tptp
60     let create_opname = create_opname
61     let create_condition = create_condition
62     let create_parent = create_parent
63     let create_dform = create_dform
64     let create_prec = create_prec
65     let create_prec_rel = create_prec_rel
66     let create_resource = create_resource
67     let create_infix = create_infix
68     let create_ml = create_ml
69    
70     (*
71     * View, close, check object.
72     * An object is not installed until it is checked.
73     *)
74     let view = view
75     let ls = ls
76    
77     (*
78     * Editing commands.
79     *)
80     let set_goal = set_goal
81     let set_redex = set_redex
82     let set_contractum = set_contractum
83     let set_assumptions = set_assumptions
84     let set_params = set_params
85     let check = check
86     let expand = expand
87    
88     (*
89     * Proof editing.
90     *)
91     let root = root
92     let up = up
93     let down = down
94     let goal = goal
95     let refine = refine
96     let undo = undo
97     let fold = fold
98     let fold_all = fold_all
99    
100     (*
101     * Nuprl5 interface.
102     *)
103     let edit_list_modules = edit_list_modules
104     let edit_list_module = edit_list_module
105     let edit_list_parents = edit_list_parents
106     let edit_list_dforms = edit_list_dforms
107     let edit_list_precs = edit_list_precs
108     let edit_list_prec_rels = edit_list_prec_rels
109     let edit_create_thm = edit_create_thm
110     let edit_cd_thm = edit_cd_thm
111     let edit_refine = edit_refine
112     let edit_node = edit_node
113     let edit_undo = edit_undo
114    
115     let _ = Shell.main ()
116    
117     (*
118     * -*-
119     * Local Variables:
120     * Caml-master: "refiner"
121     * End:
122     * -*-
123     *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26