/[mojave]
ViewVC logotype

Revision 2753


Jump to revision: Previous Next
Author: jyh
Date: Fri Jun 25 00:19:15 1999 UTC (22 years, 1 month ago)
Changed paths: 139 (showing only 100; show all)
Log Message:
These are some minor changes to make things work better.  Changed
meaning of ThinOption in elim_resource: it now means to thin the hyp
by default, unless overridden by thinningT false.

Fixed some proof operations.  Added "move_to_assum" command to take
the current subgoal and make it an extra assumption of the entire
proof (it may not work at the moment).

ls now takes a _string_ argument.  Use ls "u";; to display only the
unproved rules in the current module.

Proved many membership variants of the standard type constructors,
but there are a few more to go.  When you are defining theories, I
believe you should use membership, not equality.  After all, equality
is derivable from membership, and membership is a lot easier.

Still to go: ASCII format proof files; save proofs _without_ extracts
by default.  The expand () function does not reexpand proofs correctly.
A few problems with proof navigation.


Changed paths

Path Details
Directorymetaprl/Makefile modified , text changed
Directorymetaprl/editor/java/ modified , props changed
Directorymetaprl/editor/java/InText.java modified , text changed
Directorymetaprl/editor/java/Makefile added
Directorymetaprl/editor/java/ModeLine.java modified , text changed
Directorymetaprl/editor/java/Nuprl.java added
Directorymetaprl/editor/java/NuprlArgumentToken.java modified , text changed
Directorymetaprl/editor/java/NuprlAuthorization.java modified , text changed
Directorymetaprl/editor/java/NuprlBus.java modified , text changed
Directorymetaprl/editor/java/NuprlBusClient.java modified , text changed
Directorymetaprl/editor/java/NuprlBusEndpoint.java modified , text changed
Directorymetaprl/editor/java/NuprlBusMessage.java modified , text changed
Directorymetaprl/editor/java/NuprlBusPort.java modified , text changed
Directorymetaprl/editor/java/NuprlClient.java modified , text changed
Directorymetaprl/editor/java/NuprlCommand.java modified , text changed
Directorymetaprl/editor/java/NuprlCommandToken.java modified , text changed
Directorymetaprl/editor/java/NuprlConstants.java modified , text changed
Directorymetaprl/editor/java/NuprlContext.java modified , text changed
Directorymetaprl/editor/java/NuprlControl.java modified , text changed
Directorymetaprl/editor/java/NuprlControlToken.java modified , text changed
Directorymetaprl/editor/java/NuprlDataToken.java modified , text changed
Directorymetaprl/editor/java/NuprlDebug.java modified , text changed
Directorymetaprl/editor/java/NuprlEscapedToken.java modified , text changed
Directorymetaprl/editor/java/NuprlException.java modified , text changed
Directorymetaprl/editor/java/NuprlFrame.java modified , text changed
Directorymetaprl/editor/java/NuprlHost.java modified , text changed
Directorymetaprl/editor/java/NuprlHyperlinkToken.java modified , text changed
Directorymetaprl/editor/java/NuprlInternalFrame.java modified , text changed
Directorymetaprl/editor/java/NuprlLogin.java modified , text changed
Directorymetaprl/editor/java/NuprlManager.java modified , text changed
Directorymetaprl/editor/java/NuprlMenu.java modified , text changed
Directorymetaprl/editor/java/NuprlOptionBlockToken.java modified , text changed
Directorymetaprl/editor/java/NuprlOptionRequestToken.java modified , text changed
Directorymetaprl/editor/java/NuprlOptionResponseToken.java modified , text changed
Directorymetaprl/editor/java/NuprlOptionSBToken.java modified , text changed
Directorymetaprl/editor/java/NuprlOptionToken.java modified , text changed
Directorymetaprl/editor/java/NuprlPrlToken.java modified , text changed
Directorymetaprl/editor/java/NuprlProof.java modified , text changed
Directorymetaprl/editor/java/NuprlSyncToken.java modified , text changed
Directorymetaprl/editor/java/NuprlTerm.java added
Directorymetaprl/editor/java/NuprlText.java modified , text changed
Directorymetaprl/editor/java/NuprlToken.java modified , text changed
Directorymetaprl/editor/java/NuprlTokenInputStream.java modified , text changed
Directorymetaprl/editor/java/NuprlURLToken.java modified , text changed
Directorymetaprl/editor/java/OutText.java modified , text changed
Directorymetaprl/editor/java/PromptPasswordRecognizer.java modified , text changed
Directorymetaprl/editor/java/PromptRecognizer.java modified , text changed
Directorymetaprl/editor/java/PromptUserRecognizer.java modified , text changed
Directorymetaprl/editor/java/Semaphore.java added
Directorymetaprl/editor/java/StringBooleanFunction.java modified , text changed
Directorymetaprl/editor/java/StringIntFunction.java modified , text changed
Directorymetaprl/editor/java/StringTokenizer.java modified , text changed
Directorymetaprl/editor/java/Target.java modified , text changed
Directorymetaprl/editor/java/TtyArea.java modified , text changed
Directorymetaprl/editor/ml/mp.ml modified , text changed
Directorymetaprl/editor/ml/mp.mli modified , text changed
Directorymetaprl/editor/ml/mp_top.ml modified , text changed
Directorymetaprl/editor/ml/package_info.ml modified , text changed
Directorymetaprl/editor/ml/package_sig.mlz modified , text changed
Directorymetaprl/editor/ml/proof_edit.ml modified , text changed
Directorymetaprl/editor/ml/proof_edit.mli modified , text changed
Directorymetaprl/editor/ml/shell.ml modified , text changed
Directorymetaprl/editor/ml/shell_http.ml modified , text changed
Directorymetaprl/editor/ml/shell_mp.ml modified , text changed
Directorymetaprl/editor/ml/shell_package.ml modified , text changed
Directorymetaprl/editor/ml/shell_rewrite.ml modified , text changed
Directorymetaprl/editor/ml/shell_root.ml modified , text changed
Directorymetaprl/editor/ml/shell_rule.ml modified , text changed
Directorymetaprl/editor/ml/shell_sig.mlz modified , text changed
Directorymetaprl/editor/ml/shell_state.ml modified , text changed
Directorymetaprl/filter/filter_prog.ml modified , text changed
Directorymetaprl/filter/filter_summary.ml modified , text changed
Directorymetaprl/filter/filter_summary.mli modified , text changed
Directorymetaprl/refiner/refiner/refine.ml modified , text changed
Directorymetaprl/refiner/reflib/mp_resource.ml modified , text changed
Directorymetaprl/refiner/reflib/mp_resource.mli modified , text changed
Directorymetaprl/refiner/reflib/rformat.ml modified , text changed
Directorymetaprl/theories/base/Makefile modified , text changed
Directorymetaprl/theories/base/base_dtactic.ml modified , text changed
Directorymetaprl/theories/base/base_dtactic.mli modified , text changed
Directorymetaprl/theories/base/base_rewrite.ml added
Directorymetaprl/theories/base/base_rewrite.mli added
Directorymetaprl/theories/base/base_theory.mlz modified , text changed
Directorymetaprl/theories/base/summary.ml modified , text changed
Directorymetaprl/theories/boot/proof_boot.ml modified , text changed
Directorymetaprl/theories/boot/proof_term_boot.ml modified , text changed
Directorymetaprl/theories/boot/tactic_boot_sig.mlz modified , text changed
Directorymetaprl/theories/fol/Makefile modified , text changed
Directorymetaprl/theories/fol/fol_all.ml modified , text changed
Directorymetaprl/theories/fol/fol_and.ml modified , text changed
Directorymetaprl/theories/fol/fol_exists.ml modified , text changed
Directorymetaprl/theories/fol/fol_or.ml modified , text changed
Directorymetaprl/theories/itt/Makefile modified , text changed
Directorymetaprl/theories/itt/itt_atom_bool.ml modified , text changed
Directorymetaprl/theories/itt/itt_bool.ml modified , text changed
Directorymetaprl/theories/itt/itt_bool.mli modified , text changed
Directorymetaprl/theories/itt/itt_bool.prlb modified , text changed
Directorymetaprl/theories/itt/itt_bunion.ml modified , text changed
Directorymetaprl/theories/itt/itt_collection.ml modified , text changed
Directorymetaprl/theories/itt/itt_dfun.ml modified , text changed
[...]

  ViewVC Help
Powered by ViewVC 1.1.26