/[mojave]/metaprl/theories/itt
ViewVC logotype

Index of /metaprl/theories/itt

Files shown:132
Directory revision: 2922 (of 13286)
Sticky Revision:


File Rev. Age Author Last log entry
 Parent Directory        
.cprc  2032  24 years  jyh   This is the initial checkin of Nuprl-Light. I am porting the editor, so it is no…
Makefile  2901  21 years  nogin   Added profiling comtrol to some tests Added explicit include of the mk/preface …
README.uue  2032  24 years  jyh   This is the initial checkin of Nuprl-Light. I am porting the editor, so it is no…
itt_arith.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_arith.mli  2668  22 years  jyh   Added ML side-conditions, so that rewrites and rules can be defined with ML code…
itt_arith.prla  2906  21 years  jyh   Itt_bool now expands.
itt_atom.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_atom.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_atom.prla  2906  21 years  jyh   Itt_bool now expands.
itt_atom_bool.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_atom_bool.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_atom_bool.prla  2906  21 years  jyh   Itt_bool now expands.
itt_bisect.ml  2906  21 years  jyh   Itt_bool now expands.
itt_bisect.mli  2659  22 years  nogin   - Fixed a bug in Term_ds: The code responsible for renaming bound variables was …
itt_bisect.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_bool.ml  2906  21 years  jyh   Itt_bool now expands.
itt_bool.mli  2753  22 years  jyh   These are some minor changes to make things work better. Changed meaning of Thi…
itt_bool.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_bunion.ml  2911  21 years  jyh   Planning for update to .prla files.
itt_bunion.mli  2805  22 years  nogin   Some theories still had Itt_squash!squash instead of Base_trivial!squash - fixed…
itt_bunion.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_collection.ml  2803  22 years  nogin   Fixed intro/elim annotations in itt_collection
itt_collection.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_collection.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_decidable.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_decidable.mli  2773  22 years  nogin   I wrote a decideT tactic, similar to Nuprl4 Decide tactic. We need to prove som…
itt_decidable.prla  2906  21 years  jyh   Itt_bool now expands.
itt_decidable.prlb  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_derive.ml  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_derive.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_derive.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dfun.ml  2911  21 years  jyh   Planning for update to .prla files.
itt_dfun.mli  2911  21 years  jyh   Planning for update to .prla files.
itt_dfun.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dprod.ml  2911  21 years  jyh   Planning for update to .prla files.
itt_dprod.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_dprod.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dprod_imp.ml  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dprod_imp.mli  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_dprod_imp.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_equal.ml  2917  21 years  nogin   Efficiency: Another 6% on p4.ml
itt_equal.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_equal.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_esquash.ml  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_esquash.mli  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_esquash.prla  2906  21 years  jyh   Itt_bool now expands.
itt_ext_equal.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_ext_equal.mli  2494  22 years  jyh   I changed all the obvious places of Nuprl-Light, NL, nl, or any other instance t…
itt_ext_equal.prla  2906  21 years  jyh   Itt_bool now expands.
itt_fset.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_fset.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_fset.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_fun.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_fun.mli  2753  22 years  jyh   These are some minor changes to make things work better. Changed meaning of Thi…
itt_fun.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_int.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_int.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_int.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_int_bool.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_int_bool.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_int_bool.prla  2906  21 years  jyh   Itt_bool now expands.
itt_isect.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_isect.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_isect.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_list.ml  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_list.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_list.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_list2.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_list2.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_list2.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_logic.ml  2922  21 years  lolorigo   added/improved functionality for metaprl/jprover/nuprl5 io
itt_logic.mli  2921  21 years  steph   ---------------------------------------------------------------------- Enter …
itt_logic.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_prec.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_prec.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_prec.prla  2906  21 years  jyh   Itt_bool now expands.
itt_prod.ml  2911  21 years  jyh   Planning for update to .prla files.
itt_prod.mli  2911  21 years  jyh   Planning for update to .prla files.
itt_prod.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_prop_decide.ml  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_prop_decide.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_prop_decide.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_quotient.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_quotient.mli  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_quotient.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_rfun.ml  2911  21 years  jyh   Planning for update to .prla files.
itt_rfun.mli  2911  21 years  jyh   Planning for update to .prla files.
itt_rfun.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_set.ml  2906  21 years  jyh   Itt_bool now expands.
itt_set.mli  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_set.prla  2906  21 years  jyh   Itt_bool now expands.
itt_sort.ml  2828  21 years  nogin   Renamed break -> hbreak (dforms construction) to be more consistent.
itt_sort.mli  2795  22 years  nogin   Changed the definition of compare_lt from (lt a b) to assert(lt a b). That allow…
itt_sort.prla  2906  21 years  jyh   Itt_bool now expands.
itt_squash.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_squash.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_squash.prla  2906  21 years  jyh   Itt_bool now expands.
itt_srec.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_srec.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_srec.prla  2906  21 years  jyh   Itt_bool now expands.
itt_struct.ml  2903  21 years  nogin   - The strict rewriter mode allowed me to replace the ml_rule thin with an ordina…
itt_struct.mli  2753  22 years  jyh   These are some minor changes to make things work better. Changed meaning of Thi…
itt_struct.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_subtype.ml  2906  21 years  jyh   Itt_bool now expands.
itt_subtype.mli  2906  21 years  jyh   Itt_bool now expands.
itt_subtype.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_test.ml  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_test.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_test.prla  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_theory.ml  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_theory.mli  2812  21 years  jyh   Finally fixed the tutorial so that we have a derivation of classical first-order…
itt_theory.prla  2906  21 years  jyh   Itt_bool now expands.
itt_tsub.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_tsub.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_tunion.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_tunion.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_tunion.prla  2906  21 years  jyh   Itt_bool now expands.
itt_union.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_union.mli  2753  22 years  jyh   These are some minor changes to make things work better. Changed meaning of Thi…
itt_union.prla  2912  21 years  jyh   Most of the theories in Itt now expand without errors. One exception is Itt_fset…
itt_unit.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_unit.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_unit.prla  2906  21 years  jyh   Itt_bool now expands.
itt_void.ml  2822  21 years  nogin   Added new function to mp_debug let show_loading s = if !debug_load then Printf.e…
itt_void.mli  2743  22 years  jyh   This is a major release; I bumped the release number to 0.6. WARNING: There are …
itt_void.prla  2906  21 years  jyh   Itt_bool now expands.
itt_w.ml  2808  21 years  jyh   I added a TeX mode for display. This was a quick hack, and it it _not_ the way …
itt_w.mli  2674  22 years  nogin   I removed @ from the parameter syntax for meta-parameters. Now [xxx:s] is parsed…
itt_w.prla  2906  21 years  jyh   Itt_bool now expands.
itt_well_founded.ml  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_well_founded.mli  2775  22 years  jyh   Things seem to be working pretty smoothly now. This is mostly minor fixes. Sti…
itt_well_founded.prla  2906  21 years  jyh   Itt_bool now expands.

Properties

Name Value
svn:ignore *.cm* Makefile.dep *.p4* *.ppo *.run *.opt ocamlprof.dump gmon.out *.prlb

  ViewVC Help
Powered by ViewVC 1.1.26