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 
* Camlmaster: "refiner" 
121 
* End: 
122 
* * 
123 
*) 