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

Contents of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2604 - (show annotations) (download)
Thu Mar 4 15:02:04 1999 UTC (22 years, 4 months ago) by lolorigo
File size: 3350 byte(s)
Implemented access to rewrites and fixed saving of theories in nuprl/mp link

1 (*
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_all = edit_list_module_all
105 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
108 let edit_list_dforms = edit_list_dforms
109 let edit_list_precs = edit_list_precs
110 let edit_list_prec_rels = edit_list_prec_rels
111 let edit_create_thm = edit_create_thm
112 let edit_create_rw = edit_create_rw
113 let edit_cd_thm = edit_cd_thm
114 let edit_set_goal = edit_set_goal
115 let edit_set_redex = edit_set_redex
116 let edit_set_contractum = edit_set_contractum
117 let edit_set_assumptions = edit_set_assumptions
118 let edit_set_params = edit_set_params
119 let edit_refine = edit_refine
120 let edit_node = edit_node
121 let edit_save = edit_save
122 let edit_undo = edit_undo
123
124 let _ = Shell.main ()
125
126 (*
127 * -*-
128 * Local Variables:
129 * Caml-master: "refiner"
130 * End:
131 * -*-
132 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26