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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2494 - (show 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 (*
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