/[mojave]
ViewVC logotype

Revision 2525


Jump to revision: Previous Next
Author: jyh
Date: Mon Dec 28 21:07:52 1998 UTC (22 years, 7 months ago)
Changed paths: 139 (showing only 100; show all)
Log Message:
Numerous minor changes.

Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.

Added initial reflection theory.  Terms are quotiented by
alpha-equality, so normal well-formedness proofs are difficult,
and more work needs to be done to define free variables and
substitution.


Changed paths

Path Details
Directorymetaprl/editor/ml/mp_fol_type2.txt added
Directorymetaprl/editor/ml/mptop modified , text changed
Directorymetaprl/editor/ml/package_info.ml modified , text changed
Directorymetaprl/editor/ml/shell.ml modified , text changed
Directorymetaprl/editor/ml/shell_mp.ml modified , text changed
Directorymetaprl/editor/ml/shell_rewrite.ml modified , text changed
Directorymetaprl/editor/ml/shell_rule.ml modified , text changed
Directorymetaprl/editor/ml/tutorial.ml added
Directorymetaprl/editor/ml/tutorial_itt.ml added
Directorymetaprl/editor/ml/w.ml modified , text changed
Directorymetaprl/editor/ml/x.ml modified , text changed
Directorymetaprl/editor/ml/y.ml modified , text changed
Directorymetaprl/lib/mbs-mpl.txt added
Directorymetaprl/mbs-mpl.txt deleted
Directorymetaprl/mllib/splay_table.mli modified , text changed
Directorymetaprl/refiner/refiner/refine.mlp modified , text changed
Directorymetaprl/refiner/refsig/refine_sig.ml modified , text changed
Directorymetaprl/refiner/refsig/term_addr_sig.ml modified , text changed
Directorymetaprl/refiner/refsig/term_op_sig.ml modified , text changed
Directorymetaprl/refiner/term_ds/term_addr_ds.mlp modified , text changed
Directorymetaprl/refiner/term_ds/term_op_ds.mlp modified , text changed
Directorymetaprl/refiner/term_ds/term_subst_ds.mlp modified , text changed
Directorymetaprl/refiner/term_gen/term_addr_gen.mlp modified , text changed
Directorymetaprl/refiner/term_std/term_op_std.mlp 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.mli modified , text changed
Directorymetaprl/theories/base/base_theory.mlz modified , text changed
Directorymetaprl/theories/base/typeinf.ml modified , text changed
Directorymetaprl/theories/base/typeinf.mli modified , text changed
Directorymetaprl/theories/fol/Makefile modified , text changed
Directorymetaprl/theories/fol/fol_all.ml modified , text changed
Directorymetaprl/theories/fol/fol_all_itt.ml added
Directorymetaprl/theories/fol/fol_all_itt.mli added
Directorymetaprl/theories/fol/fol_all_itt.prlb added
Directorymetaprl/theories/fol/fol_bisect_itt.ml added
Directorymetaprl/theories/fol/fol_bisect_itt.mli added
Directorymetaprl/theories/fol/fol_ctheory.prlb added
Directorymetaprl/theories/fol/fol_exists.ml modified , text changed
Directorymetaprl/theories/fol/fol_implies.ml modified , text changed
Directorymetaprl/theories/fol/fol_not.prlb modified , text changed
Directorymetaprl/theories/fol/fol_theory.ml added
Directorymetaprl/theories/fol/fol_theory.mli added
Directorymetaprl/theories/fol/fol_theory.prlb added
Directorymetaprl/theories/fol/fol_type.ml modified , text changed
Directorymetaprl/theories/fol/fol_type.mli modified , text changed
Directorymetaprl/theories/fol/fol_type_itt.ml added
Directorymetaprl/theories/fol/fol_type_itt.mli added
Directorymetaprl/theories/fol/fol_type_itt.prlb added
Directorymetaprl/theories/fol/fol_univ.ml modified , text changed
Directorymetaprl/theories/fol/fol_univ.mli modified , text changed
Directorymetaprl/theories/fol/fol_univ_itt.ml added
Directorymetaprl/theories/fol/fol_univ_itt.mli added
Directorymetaprl/theories/fol/fol_univ_itt.prlb added
Directorymetaprl/theories/itt/Makefile modified , text changed
Directorymetaprl/theories/itt/itt_atom.ml modified , text changed
Directorymetaprl/theories/itt/itt_atom.mli modified , text changed
Directorymetaprl/theories/itt/itt_atom_bool.ml added
Directorymetaprl/theories/itt/itt_atom_bool.mli added
Directorymetaprl/theories/itt/itt_bisect.ml added
Directorymetaprl/theories/itt/itt_bisect.mli added
Directorymetaprl/theories/itt/itt_bisect.prlb added
Directorymetaprl/theories/itt/itt_bool.ml modified , text changed
Directorymetaprl/theories/itt/itt_bool.mli modified , text changed
Directorymetaprl/theories/itt/itt_bool.prlb added
Directorymetaprl/theories/itt/itt_bunion.ml added
Directorymetaprl/theories/itt/itt_bunion.mli added
Directorymetaprl/theories/itt/itt_bunion.prlb added
Directorymetaprl/theories/itt/itt_dprod.ml modified , text changed
Directorymetaprl/theories/itt/itt_equal.ml modified , text changed
Directorymetaprl/theories/itt/itt_equal.mli modified , text changed
Directorymetaprl/theories/itt/itt_equal.prlb modified , text changed
Directorymetaprl/theories/itt/itt_fset.ml added
Directorymetaprl/theories/itt/itt_fset.mli added
Directorymetaprl/theories/itt/itt_fset.prlb added
Directorymetaprl/theories/itt/itt_int.ml modified , text changed
Directorymetaprl/theories/itt/itt_int.mli modified , text changed
Directorymetaprl/theories/itt/itt_int_bool.ml modified , text changed
Directorymetaprl/theories/itt/itt_isect.ml modified , text changed
Directorymetaprl/theories/itt/itt_isect.mli modified , text changed
Directorymetaprl/theories/itt/itt_isect.prlb added
Directorymetaprl/theories/itt/itt_list.ml modified , text changed
Directorymetaprl/theories/itt/itt_list.mli modified , text changed
Directorymetaprl/theories/itt/itt_list.prlb added
Directorymetaprl/theories/itt/itt_list2.ml added
Directorymetaprl/theories/itt/itt_list2.mli added
Directorymetaprl/theories/itt/itt_list2.prlb added
Directorymetaprl/theories/itt/itt_logic.ml modified , text changed
Directorymetaprl/theories/itt/itt_logic.mli modified , text changed
Directorymetaprl/theories/itt/itt_quotient.ml modified , text changed
Directorymetaprl/theories/itt/itt_quotient.mli modified , text changed
Directorymetaprl/theories/itt/itt_rfun.ml modified , text changed
Directorymetaprl/theories/itt/itt_set.ml modified , text changed
Directorymetaprl/theories/itt/itt_set.mli modified , text changed
Directorymetaprl/theories/itt/itt_srec.ml modified , text changed
Directorymetaprl/theories/itt/itt_srec.mli modified , text changed
Directorymetaprl/theories/itt/itt_struct.ml modified , text changed
Directorymetaprl/theories/itt/itt_subtype.ml modified , text changed
Directorymetaprl/theories/itt/itt_subtype.mli modified , text changed
Directorymetaprl/theories/itt/itt_theory.ml modified , text changed
[...]

  ViewVC Help
Powered by ViewVC 1.1.26