Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -300 -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
Fri, 04 Dec 2009 21:43:29 +0100 Christian Urban merged file | diff | annotate
Fri, 04 Dec 2009 21:42:55 +0100 Christian Urban not yet quite functional treatment of constants file | diff | annotate
Fri, 04 Dec 2009 19:47:58 +0100 Cezary Kaliszyk Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :) file | diff | annotate
Fri, 04 Dec 2009 19:06:53 +0100 Cezary Kaliszyk Changing FOCUS to CSUBGOAL (part 1) file | diff | annotate
Fri, 04 Dec 2009 17:50:02 +0100 Cezary Kaliszyk Minor renames and moving file | diff | annotate
Fri, 04 Dec 2009 17:36:45 +0100 Cezary Kaliszyk Cleaning/review of QuotScript. file | diff | annotate
Fri, 04 Dec 2009 17:15:55 +0100 Cezary Kaliszyk More cleaning file | diff | annotate
Fri, 04 Dec 2009 16:53:11 +0100 Cezary Kaliszyk more name cleaning and removing file | diff | annotate
Fri, 04 Dec 2009 16:40:23 +0100 Cezary Kaliszyk More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList file | diff | annotate
Fri, 04 Dec 2009 16:12:40 +0100 Cezary Kaliszyk Cleaning & Renaming coming from QuotList file | diff | annotate
Fri, 04 Dec 2009 15:50:57 +0100 Cezary Kaliszyk Even more name changes and cleaning file | diff | annotate
Fri, 04 Dec 2009 15:41:09 +0100 Cezary Kaliszyk More code cleaning and name changes file | diff | annotate
Fri, 04 Dec 2009 15:18:33 +0100 Cezary Kaliszyk More name changes file | diff | annotate
Fri, 04 Dec 2009 14:35:36 +0100 Cezary Kaliszyk code cleaning and renaming file | diff | annotate
Fri, 04 Dec 2009 14:11:20 +0100 Cezary Kaliszyk merge file | diff | annotate
Fri, 04 Dec 2009 14:11:03 +0100 Cezary Kaliszyk Removed previous inj_repabs_tac file | diff | annotate
Fri, 04 Dec 2009 13:58:23 +0100 Christian Urban some tuning file | diff | annotate
Fri, 04 Dec 2009 12:21:15 +0100 Cezary Kaliszyk merge file | diff | annotate
Fri, 04 Dec 2009 12:20:49 +0100 Cezary Kaliszyk rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification. file | diff | annotate
Fri, 04 Dec 2009 11:34:49 +0100 Christian Urban merged file | diff | annotate
Fri, 04 Dec 2009 11:34:21 +0100 Christian Urban merged file | diff | annotate
Fri, 04 Dec 2009 11:33:58 +0100 Cezary Kaliszyk Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations. file | diff | annotate
Fri, 04 Dec 2009 11:06:43 +0100 Cezary Kaliszyk compose_tac instead of rtac to avoid unification; some code cleaning. file | diff | annotate
Fri, 04 Dec 2009 10:36:35 +0100 Cezary Kaliszyk Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof. file | diff | annotate
Fri, 04 Dec 2009 10:12:17 +0100 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster. file | diff | annotate
Fri, 04 Dec 2009 09:33:32 +0100 Cezary Kaliszyk Fixes after big merge. file | diff | annotate
Fri, 04 Dec 2009 09:25:27 +0100 Cezary Kaliszyk The big merge; probably non-functional. file | diff | annotate
Fri, 04 Dec 2009 09:08:51 +0100 Cezary Kaliszyk Testing the new tactic everywhere file | diff | annotate
Fri, 04 Dec 2009 09:01:13 +0100 Cezary Kaliszyk First version of the deterministic rep-abs-inj-tac. file | diff | annotate
Fri, 04 Dec 2009 09:18:46 +0100 Cezary Kaliszyk Changing = to \<equiv> in case if we want to use simp. file | diff | annotate
Fri, 04 Dec 2009 09:10:31 +0100 Cezary Kaliszyk Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac file | diff | annotate
Fri, 04 Dec 2009 08:19:56 +0100 Cezary Kaliszyk merge file | diff | annotate
Fri, 04 Dec 2009 08:18:38 +0100 Cezary Kaliszyk Made your version work again with LIST_REL_EQ. file | diff | annotate
Thu, 03 Dec 2009 19:06:14 +0100 Christian Urban the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied file | diff | annotate
Thu, 03 Dec 2009 15:03:31 +0100 Christian Urban removed quot argument...not all examples work anymore file | diff | annotate
Thu, 03 Dec 2009 14:02:05 +0100 Christian Urban merged file | diff | annotate
Thu, 03 Dec 2009 13:59:53 +0100 Christian Urban first version of internalised quotient theorems; added FIXME-TODO file | diff | annotate
Thu, 03 Dec 2009 11:40:10 +0100 Christian Urban further dead code file | diff | annotate
Thu, 03 Dec 2009 13:56:59 +0100 Cezary Kaliszyk Reintroduced varifyT; we still need it for permutation definition. file | diff | annotate
Thu, 03 Dec 2009 12:33:05 +0100 Cezary Kaliszyk Fixed previous mistake file | diff | annotate
Thu, 03 Dec 2009 12:31:05 +0100 Cezary Kaliszyk defs used automatically by clean_tac file | diff | annotate
Thu, 03 Dec 2009 11:58:46 +0100 Cezary Kaliszyk removing unused code file | diff | annotate
Thu, 03 Dec 2009 11:33:24 +0100 Christian Urban deleted some dead code file | diff | annotate
Thu, 03 Dec 2009 11:28:19 +0100 Cezary Kaliszyk Included all_prs and ex_prs in the lambda_prs conversion. file | diff | annotate
Thu, 03 Dec 2009 02:53:54 +0100 Christian Urban further simplification file | diff | annotate
Thu, 03 Dec 2009 02:18:21 +0100 Christian Urban simplified lambda_prs_conv file | diff | annotate
Wed, 02 Dec 2009 23:31:30 +0100 Christian Urban deleted now obsolete argument rty everywhere file | diff | annotate
Wed, 02 Dec 2009 23:11:50 +0100 Christian Urban deleted tests at the beginning of QuotMain file | diff | annotate
Wed, 02 Dec 2009 20:54:59 +0100 Cezary Kaliszyk Experiments with OPTION_map file | diff | annotate
Wed, 02 Dec 2009 17:16:44 +0100 Cezary Kaliszyk merge file | diff | annotate
Wed, 02 Dec 2009 17:15:36 +0100 Cezary Kaliszyk More experiments with higher order quotients and theorems with non-lifted constants. file | diff | annotate
Wed, 02 Dec 2009 16:12:41 +0100 Christian Urban merged file | diff | annotate
Wed, 02 Dec 2009 14:11:46 +0100 Cezary Kaliszyk New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet. file | diff | annotate
Wed, 02 Dec 2009 12:07:54 +0100 Cezary Kaliszyk Fixed unlam for non-abstractions and updated list_induct_part proof. file | diff | annotate
Wed, 02 Dec 2009 11:30:40 +0100 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically. file | diff | annotate
Wed, 02 Dec 2009 10:56:35 +0100 Cezary Kaliszyk The conversion approach works. file | diff | annotate
Wed, 02 Dec 2009 07:21:10 +0100 Cezary Kaliszyk Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE. file | diff | annotate
Tue, 01 Dec 2009 19:18:43 +0100 Cezary Kaliszyk back in working state file | diff | annotate
Tue, 01 Dec 2009 19:01:51 +0100 Cezary Kaliszyk clean file | diff | annotate
Tue, 01 Dec 2009 18:51:14 +0100 Christian Urban fixed previous commit file | diff | annotate
less more (0) -300 -100 -60 tip
nominal2