[nogin] Moved nthAssumT from Itt_struct to Itt_squash and made it do_Mon Sep 19 02:57:55 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-57-55-890113000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-57-55-890113000-PDT.html[nogin] src mode dform fixes._Mon Sep 19 02:58:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-30-455909000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-30-455909000-PDT.html[kopylov] _ added rules applyEquality to intro resource_Mon Sep 19 02:58:30 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-30-880685000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-30-880685000-PDT.html[nogin] Fixed a minor bug._Mon Sep 19 02:58:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-54-611144000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-54-611144000-PDT.html[kopylov] Fixed some proofs._Mon Sep 19 02:58:54 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-54-979393000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-58-54-979393000-PDT.html[nogin] Better sequent matching code._Mon Sep 19 02:59:03 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-03-635057000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-03-635057000-PDT.html[nogin] JProver shouldn_t do _make_opname_ all the time._Mon Sep 19 02:59:03 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-03-993056000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-03-993056000-PDT.html[kopylov] _ Now substitution _s1_s2 in S_ for conclution _t in T[s1]_ produces a wf subgoal_Mon Sep 19 02:59:04 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-04-584439000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-04-584439000-PDT.html[nogin] Made var_subst a little more general._Mon Sep 19 02:59:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-10-216070000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-10-216070000-PDT.html[nogin] Fixed the bug in match_terms that was causing the stack overflow errors_Mon Sep 19 02:59:10 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-10-662411000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-10-662411000-PDT.html[nogin] I have changed the way autoT works._Mon Sep 19 02:59:11 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-11-067592000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-11-067592000-PDT.html[nogin] _ Added __H_ x_ _A_ _J[_x] __ _type___A__ to autoT_Mon Sep 19 02:59:29 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-29-929803000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-02-59-29-929803000-PDT.html[kopylov] Fixed two proofs_Mon Sep 19 03:00:35 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-35-273061000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-35-273061000-PDT.html[kopylov] _ Fixed some bugs in Itt_w__Mon Sep 19 03:00:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-37-077631000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-37-077631000-PDT.html[kopylov] _ Changed intro rule for the set type according to Alexey_s beter_itt._Mon Sep 19 03:00:39 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-39-856769000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-39-856769000-PDT.html[nogin] Added elim_typeinf and intro_typeinf functions_Mon Sep 19 03:00:43 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-43-934308000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-43-934308000-PDT.html[nogin] More itt_fset fixes._Mon Sep 19 03:00:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-44-412542000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-44-412542000-PDT.html[nogin] Use String.concat instead of String_util.concat_Mon Sep 19 03:00:50 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-50-104608000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-50-104608000-PDT.html[kopylov] Fix some proofs_Mon Sep 19 03:00:53 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-53-180717000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-00-53-180717000-PDT.html[nogin] Numerous display form updates._Mon Sep 19 03:01:08 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-08-365884000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-08-365884000-PDT.html[nogin] _ Rewrote the Itt_esquash theory based on my _better_tt_ ideas._Mon Sep 19 03:01:09 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-09-319134000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-09-319134000-PDT.html[nogin] _ trivialT can now do equalRefT and equalSymT when necessary to match_Mon Sep 19 03:01:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-17-127610000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-17-127610000-PDT.html[nogin] Finished fixing cfol proofs._Mon Sep 19 03:01:36 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-36-201084000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-36-201084000-PDT.html[nogin] FOL theory is now complete._Mon Sep 19 03:01:38 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-38-172917000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-38-172917000-PDT.html[nogin] I_ve removed old Itt_int_ theories and switched all the ITT to Yegor_s_Mon Sep 19 03:01:42 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-42-093931000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-01-42-093931000-PDT.html[nogin] ._Mon Sep 19 03:02:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-27-363094000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-27-363094000-PDT.html[nogin] _ The Itt_quotient theory is now a theory of _intensional_ quotient type_Mon Sep 19 03:02:27 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-27-875588000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-27-875588000-PDT.html[nogin] When eliminating a quotient hyp, dT will now use a simplier rule_Mon Sep 19 03:02:33 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-33-533366000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-33-533366000-PDT.html[nogin] When a bound variable already exists in the goal, it should not be_Mon Sep 19 03:02:34 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-34-172759000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-34-172759000-PDT.html[nogin] Fixed more Itt_fset proofs._Mon Sep 19 03:02:37 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-37-592985000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-02-37-592985000-PDT.html[nogin] More proof fixes._Mon Sep 19 03:04:02 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-04-02-363012000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-04-02-363012000-PDT.html[nogin] _ Improved proof replay._Mon Sep 19 03:04:13 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-04-13-987453000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-04-13-987453000-PDT.html[nogin] More itt_fset fixes._Mon Sep 19 03:06:40 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-40-894121000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-40-894121000-PDT.html[nogin] Had to increase the bytecode stack size so that bytecode can handle large_Mon Sep 19 03:06:48 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-48-584120000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-48-584120000-PDT.html[nogin] _ Proved list cons_cons equality elimination._Mon Sep 19 03:06:49 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-49-121313000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-06-49-121313000-PDT.html[nogin] Itt_fset is finally complete__Mon Sep 19 03:07:17 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-17-224117000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-17-224117000-PDT.html[nogin] _ created a tcaT tactic that is equivalent to tryT _completeT autoT__Mon Sep 19 03:07:44 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-44-104192000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-44-104192000-PDT.html[nogin] _ Added a new tactic copyHypT for copying hypotheses _useful in elimination rules_._Mon Sep 19 03:07:47 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-47-341751000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-47-341751000-PDT.html[nogin] Added subtypeT function__Mon Sep 19 03:07:51 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-51-342542000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-51-342542000-PDT.html[nogin] I rewrote itt_collection using my _better_tt_ ideas and proved all the_Mon Sep 19 03:07:56 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-56-937363000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-07-56-937363000-PDT.html[kopylov] I changed the rule subtypeElimination2 and proved use_subtype1._Mon Sep 19 03:11:16 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-16-796556000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-16-796556000-PDT.html[emre] Initial import. mc is the name of Jason_s compiler project, and functional_Mon Sep 19 03:11:19 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-19-818122000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-19-818122000-PDT.html[emre] Initial import of the type system for the FIR. Not everything is here yet._Mon Sep 19 03:11:24 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-24-729385000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-24-729385000-PDT.html[nogin] Updated the _Simplified Syntax_ section of User Guide._Mon Sep 19 03:11:25 PDT 2005
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-25-723398000-PDT.html
http://svn.metaprl.org/commitlogs/metaprl/2001-07/2005-09-19-03-11-25-723398000-PDT.html