[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