Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1999-08-08 08:25:48 -0700 (Sun, 08 Aug 1999)
Revision: 2807
Log message:

      These are outdated
      

Changes  Path
Deleted metaprl/free_prlb
Deleted metaprl/update_prlb

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-08-25 12:09:25 -0700 (Wed, 25 Aug 1999)
Revision: 2808
Log message:

      I added a TeX mode for display.  This was a quick hack, and it
      it _not_ the way it should be done long term.  We should be able
      to do the formatting and indentation with boxes, etc.
      
      I added SIL.  This theory is an incomplete semantics of a
      "simple imperative language."
      

Changes  Path
+11 -5 metaprl/editor/java/Nuprl.java
+0 -0 metaprl/editor/java/Nuprl.man
+5 -3 metaprl/editor/java/NuprlManager.java
+11 -2 metaprl/editor/java/NuprlTerm.java
+2 -2 metaprl/editor/java/NuprlText.java
+0 -1 metaprl/editor/ml/display_term.ml
+14 -1 metaprl/editor/ml/proof_edit.ml
+1 -0 metaprl/editor/ml/proof_edit.mli
+8 -1 metaprl/editor/ml/shell.ml
+0 -3 metaprl/editor/ml/shell_http.ml
+15 -12 metaprl/editor/ml/shell_package.ml
+2 -0 metaprl/editor/ml/shell_rewrite.ml
+20 -13 metaprl/editor/ml/shell_root.ml
+2 -0 metaprl/editor/ml/shell_rule.ml
+1 -0 metaprl/editor/ml/shell_sig.mlz
+5 -8 metaprl/filter/boot/proof_boot.ml
+7 -8 metaprl/filter/boot/proof_term_boot.ml
+1 -1 metaprl/filter/boot/rewrite_boot.ml
+8 -2 metaprl/filter/boot/tactic_boot.ml
+3 -2 metaprl/refiner/refiner/refine.ml
+165 -0 metaprl/refiner/reflib/rformat.ml
+1 -0 metaprl/refiner/reflib/rformat.mli
+77 -0 metaprl/theories/base/base_dform.ml
+13 -21 metaprl/theories/base/base_rewrite.ml
+8 -1 metaprl/theories/base/base_rewrite.mli
+17 -9 metaprl/theories/base/summary.ml
+2 -2 metaprl/theories/itt/itt_atom.ml
+1 -1 metaprl/theories/itt/itt_atom_bool.ml
+1 -1 metaprl/theories/itt/itt_bisect.ml
+9 -9 metaprl/theories/itt/itt_bool.ml
+1 -1 metaprl/theories/itt/itt_bunion.ml
Added metaprl/theories/itt/itt_decidable.prlb
Properties metaprl/theories/itt/itt_decidable.prlb
+6 -6 metaprl/theories/itt/itt_dprod.ml
+6 -6 metaprl/theories/itt/itt_dprod_imp.ml
+6 -5 metaprl/theories/itt/itt_equal.ml
+18 -18 metaprl/theories/itt/itt_fset.ml
+8 -8 metaprl/theories/itt/itt_int.ml
+5 -5 metaprl/theories/itt/itt_int_bool.ml
+1 -1 metaprl/theories/itt/itt_isect.ml
+2 -2 metaprl/theories/itt/itt_list.ml
+7 -7 metaprl/theories/itt/itt_list2.ml
+6 -6 metaprl/theories/itt/itt_logic.ml
+1 -1 metaprl/theories/itt/itt_quotient.ml
+2 -2 metaprl/theories/itt/itt_rfun.ml
+2 -2 metaprl/theories/itt/itt_set.ml
+1 -1 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_tsub.ml
+1 -1 metaprl/theories/itt/itt_tunion.ml
+4 -4 metaprl/theories/itt/itt_union.ml
+1 -1 metaprl/theories/itt/itt_unit.ml
+1 -1 metaprl/theories/itt/itt_void.ml
+3 -3 metaprl/theories/itt/itt_w.ml
Properties metaprl/theories/sil
Added metaprl/theories/sil/Makefile
Properties metaprl/theories/sil/Makefile
Added metaprl/theories/sil/sil_itt_sos.ml
Properties metaprl/theories/sil/sil_itt_sos.ml
Added metaprl/theories/sil/sil_itt_sos.mli
Properties metaprl/theories/sil/sil_itt_sos.mli
Added metaprl/theories/sil/sil_itt_state.ml
Properties metaprl/theories/sil/sil_itt_state.ml
Added metaprl/theories/sil/sil_itt_state.mli
Properties metaprl/theories/sil/sil_itt_state.mli
Added metaprl/theories/sil/sil_itt_state_types.ml
Properties metaprl/theories/sil/sil_itt_state_types.ml
Added metaprl/theories/sil/sil_itt_state_types.mli
Properties metaprl/theories/sil/sil_itt_state_types.mli
Added metaprl/theories/sil/sil_itt_types.ml
Properties metaprl/theories/sil/sil_itt_types.ml
Added metaprl/theories/sil/sil_model.ml
Properties metaprl/theories/sil/sil_model.ml
Added metaprl/theories/sil/sil_program.ml
Properties metaprl/theories/sil/sil_program.ml
Added metaprl/theories/sil/sil_program.mli
Properties metaprl/theories/sil/sil_program.mli
Added metaprl/theories/sil/sil_programs.ml
Properties metaprl/theories/sil/sil_programs.ml
Added metaprl/theories/sil/sil_programs.mli
Properties metaprl/theories/sil/sil_programs.mli
Added metaprl/theories/sil/sil_sos.ml
Properties metaprl/theories/sil/sil_sos.ml
Added metaprl/theories/sil/sil_sos.ml.new
Properties metaprl/theories/sil/sil_sos.ml.new
Added metaprl/theories/sil/sil_sos.mli
Properties metaprl/theories/sil/sil_sos.mli
Added metaprl/theories/sil/sil_sos.mli.new
Properties metaprl/theories/sil/sil_sos.mli.new
Added metaprl/theories/sil/sil_state.ml
Properties metaprl/theories/sil/sil_state.ml
Added metaprl/theories/sil/sil_state.mli
Properties metaprl/theories/sil/sil_state.mli
Added metaprl/theories/sil/sil_state_model.ml
Properties metaprl/theories/sil/sil_state_model.ml
Added metaprl/theories/sil/sil_state_model.mli
Properties metaprl/theories/sil/sil_state_model.mli
Added metaprl/theories/sil/sil_state_type.ml
Properties metaprl/theories/sil/sil_state_type.ml
Added metaprl/theories/sil/sil_state_type.mli
Properties metaprl/theories/sil/sil_state_type.mli
Added metaprl/theories/sil/sil_state_types.ml
Properties metaprl/theories/sil/sil_state_types.ml
Added metaprl/theories/sil/sil_state_types.mli
Properties metaprl/theories/sil/sil_state_types.mli
Added metaprl/theories/sil/sil_types.ml
Properties metaprl/theories/sil/sil_types.ml
Added metaprl/theories/sil/sil_types.mli
Properties metaprl/theories/sil/sil_types.mli
Added metaprl/theories/sil/state_types.ml
Properties metaprl/theories/sil/state_types.ml
+247 -2 metaprl/theories/tactic/nuprl_font.ml
+6 -0 metaprl/theories/tactic/nuprl_font.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-08-31 10:31:53 -0700 (Tue, 31 Aug 1999)
Revision: 2809
Log message:

      Display changes to get Java to work a little better.
      

Changes  Path
+5 -1 metaprl/editor/ml/display_term.ml
+24 -1 metaprl/editor/ml/proof_edit.ml
+50 -3 metaprl/refiner/reflib/dform.ml
+8 -0 metaprl/refiner/reflib/term_match_table.ml
+0 -4 metaprl/theories/base/base_dform.ml
+3 -1 metaprl/theories/base/summary.ml
+0 -82 metaprl/theories/tactic/nuprl_font.ml