Sat, 28 Nov 2009 04:37:30 +0100 Christian Urban merged
Sat, 28 Nov 2009 04:37:04 +0100 Christian Urban fixed previous commit
Sat, 28 Nov 2009 04:02:54 +0100 Cezary Kaliszyk Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Sat, 28 Nov 2009 03:17:22 +0100 Cezary Kaliszyk Merged comment
Sat, 28 Nov 2009 03:07:38 +0100 Cezary Kaliszyk Integrated Stefan's tactic and changed substs to simps with empty context.
Sat, 28 Nov 2009 03:06:22 +0100 Christian Urban some slight tuning of the apply-tactic
Sat, 28 Nov 2009 02:54:24 +0100 Christian Urban annotated a proof with all steps and simplified LAMBDA_RES_TAC
Fri, 27 Nov 2009 18:38:44 +0100 Cezary Kaliszyk Merge
Fri, 27 Nov 2009 18:38:09 +0100 Cezary Kaliszyk The magical code from Stefan, will need to be integrated in the Simproc.
Fri, 27 Nov 2009 13:59:52 +0100 Christian Urban replaced FIRST' (map rtac list) with resolve_tac list
Fri, 27 Nov 2009 10:04:49 +0100 Cezary Kaliszyk Simplifying arguments; got rid of trans2_thm.
Fri, 27 Nov 2009 09:16:32 +0100 Cezary Kaliszyk Cleaning of LFex. Lambda_prs fails to unify in 2 places.
Fri, 27 Nov 2009 08:22:46 +0100 Cezary Kaliszyk Recommit
Fri, 27 Nov 2009 08:15:23 +0100 Cezary Kaliszyk Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Fri, 27 Nov 2009 07:16:16 +0100 Cezary Kaliszyk More cleaning in QuotMain, identity handling.
Fri, 27 Nov 2009 07:00:14 +0100 Cezary Kaliszyk Minor cleaning
Fri, 27 Nov 2009 04:02:20 +0100 Christian Urban tuned
Fri, 27 Nov 2009 03:56:18 +0100 Christian Urban some tuning
Fri, 27 Nov 2009 03:33:30 +0100 Christian Urban simplified gen_frees_tac and properly named abstracted variables
Fri, 27 Nov 2009 02:58:28 +0100 Christian Urban removed CHANGED'
Fri, 27 Nov 2009 02:55:56 +0100 Christian Urban introduced a separate lemma for id_simps
Fri, 27 Nov 2009 02:45:54 +0100 Christian Urban renamed inj_REPABS to inj_repabs_trm
Fri, 27 Nov 2009 02:44:11 +0100 Christian Urban tuned comments and moved slightly some code
Fri, 27 Nov 2009 02:35:50 +0100 Christian Urban deleted obsolete qenv code
Fri, 27 Nov 2009 02:23:49 +0100 Christian Urban renamed REGULARIZE to be regularize
Thu, 26 Nov 2009 21:16:59 +0100 Christian Urban more tuning
Thu, 26 Nov 2009 21:04:17 +0100 Christian Urban deleted get_fun_old and stuff
Thu, 26 Nov 2009 21:01:53 +0100 Christian Urban recommited changes of comments
Thu, 26 Nov 2009 20:32:56 +0100 Cezary Kaliszyk Merge Again
Thu, 26 Nov 2009 20:32:33 +0100 Cezary Kaliszyk Merged
Thu, 26 Nov 2009 20:18:36 +0100 Christian Urban tuned comments
Thu, 26 Nov 2009 19:51:31 +0100 Christian Urban some diagnostic code for r_mk_comb
Thu, 26 Nov 2009 16:23:24 +0100 Christian Urban introduced a new property for Ball and ===> on the left
Thu, 26 Nov 2009 13:52:46 +0100 Christian Urban fixed QuotList
Thu, 26 Nov 2009 13:46:00 +0100 Christian Urban changed left-res
Thu, 26 Nov 2009 12:21:47 +0100 Cezary Kaliszyk Manually regularized akind_aty_atrm.induct
Thu, 26 Nov 2009 10:52:24 +0100 Cezary Kaliszyk Playing with Monos in LFex.
Thu, 26 Nov 2009 10:32:31 +0100 Cezary Kaliszyk Fixed FSet after merge.
Thu, 26 Nov 2009 03:18:38 +0100 Christian Urban merged
Thu, 26 Nov 2009 02:31:00 +0100 Christian Urban test with monos
Wed, 25 Nov 2009 21:48:32 +0100 Cezary Kaliszyk applic_prs
Wed, 25 Nov 2009 15:43:12 +0100 Christian Urban polishing
Wed, 25 Nov 2009 15:20:10 +0100 Christian Urban reordered the code
Wed, 25 Nov 2009 14:25:29 +0100 Cezary Kaliszyk Moved exception handling to QuotMain and cleaned FSet.
Wed, 25 Nov 2009 14:16:33 +0100 Cezary Kaliszyk Merge
Wed, 25 Nov 2009 14:15:34 +0100 Cezary Kaliszyk Finished manual lifting of list_induct_part :)
Wed, 25 Nov 2009 12:27:28 +0100 Christian Urban comments tuning and slight reordering
Wed, 25 Nov 2009 11:59:49 +0100 Cezary Kaliszyk Merge
Wed, 25 Nov 2009 11:58:56 +0100 Cezary Kaliszyk More moving from QuotMain to UnusedQuotMain
Wed, 25 Nov 2009 11:46:59 +0100 Christian Urban deleted some obsolete diagnostic code
Wed, 25 Nov 2009 11:41:42 +0100 Cezary Kaliszyk Removed unused things from QuotMain.
Wed, 25 Nov 2009 10:52:21 +0100 Cezary Kaliszyk All examples work again.
Wed, 25 Nov 2009 10:39:53 +0100 Cezary Kaliszyk cleaning in MyInt
Wed, 25 Nov 2009 10:34:03 +0100 Cezary Kaliszyk lambda_prs and cleaning the existing examples.
Wed, 25 Nov 2009 03:47:07 +0100 Christian Urban merged
Wed, 25 Nov 2009 03:45:44 +0100 Christian Urban fixed the problem with generalising variables; at the moment it is quite a hack
Tue, 24 Nov 2009 20:13:16 +0100 Cezary Kaliszyk Ho-matching failures...
Tue, 24 Nov 2009 19:09:29 +0100 Christian Urban changed unification to matching
Tue, 24 Nov 2009 18:13:57 +0100 Christian Urban unification
Tue, 24 Nov 2009 18:13:18 +0100 Cezary Kaliszyk Lambda & SOLVED' for new quotient_tac
Tue, 24 Nov 2009 17:35:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 17:00:53 +0100 Cezary Kaliszyk Conversion
Tue, 24 Nov 2009 16:20:34 +0100 Cezary Kaliszyk The non-working procedure_tac.
Tue, 24 Nov 2009 16:10:31 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:31:29 +0100 Christian Urban use error instead of raising our own exception
Tue, 24 Nov 2009 15:18:00 +0100 Cezary Kaliszyk Fixes to the tactic after quotient_tac changed.
Tue, 24 Nov 2009 15:15:33 +0100 Christian Urban merged
Tue, 24 Nov 2009 15:15:10 +0100 Christian Urban added a prepare_tac
Tue, 24 Nov 2009 14:41:47 +0100 Cezary Kaliszyk TRY' for clean_tac
Tue, 24 Nov 2009 14:19:54 +0100 Cezary Kaliszyk Moved cleaning to QuotMain
Tue, 24 Nov 2009 14:16:57 +0100 Cezary Kaliszyk New cleaning tactic
Tue, 24 Nov 2009 13:46:36 +0100 Christian Urban explicit phases for the cleaning
Tue, 24 Nov 2009 12:25:04 +0100 Cezary Kaliszyk Separate regularize_tac
Tue, 24 Nov 2009 08:36:28 +0100 Cezary Kaliszyk Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Tue, 24 Nov 2009 08:35:04 +0100 Cezary Kaliszyk More fixes for inj_REPABS
Tue, 24 Nov 2009 01:36:50 +0100 Christian Urban addded a tactic, which sets up the three goals of the `algorithm'
Mon, 23 Nov 2009 23:09:03 +0100 Christian Urban fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Mon, 23 Nov 2009 22:00:54 +0100 Christian Urban merged
Mon, 23 Nov 2009 21:59:57 +0100 Christian Urban tuned some comments
Mon, 23 Nov 2009 21:56:30 +0100 Cezary Kaliszyk Another not-typechecking regularized term.
Mon, 23 Nov 2009 21:48:44 +0100 Cezary Kaliszyk domain_type in regularizing equality
Mon, 23 Nov 2009 21:12:16 +0100 Cezary Kaliszyk More theorems lifted in the goal-directed way.
Mon, 23 Nov 2009 20:10:39 +0100 Cezary Kaliszyk Finished temporary goal-directed lift_theorem wrapper.
Mon, 23 Nov 2009 16:13:19 +0100 Christian Urban merged
Mon, 23 Nov 2009 16:12:50 +0100 Christian Urban a version of inj_REPABS (needs to be looked at again later)
Mon, 23 Nov 2009 15:47:14 +0100 Cezary Kaliszyk Fixes for atomize
Mon, 23 Nov 2009 15:08:25 +0100 Cezary Kaliszyk merge
Mon, 23 Nov 2009 15:08:09 +0100 Cezary Kaliszyk lift_thm with a goal.
Mon, 23 Nov 2009 15:02:48 +0100 Christian Urban slight change in code layout
Mon, 23 Nov 2009 14:40:53 +0100 Cezary Kaliszyk Fixes for new code
Mon, 23 Nov 2009 14:32:11 +0100 Cezary Kaliszyk Removing dead code
Mon, 23 Nov 2009 14:16:41 +0100 Cezary Kaliszyk Move atomize_goal to QuotMain
Mon, 23 Nov 2009 14:05:02 +0100 Cezary Kaliszyk Removed second implementation of Regularize/Inject from FSet.
Mon, 23 Nov 2009 13:55:31 +0100 Cezary Kaliszyk Moved new repabs_inj code to QuotMain
Mon, 23 Nov 2009 13:46:14 +0100 Cezary Kaliszyk New repabs behaves the same way as old one.
Mon, 23 Nov 2009 13:24:12 +0100 Christian Urban code review with Cezary
Mon, 23 Nov 2009 10:26:59 +0100 Cezary Kaliszyk The other branch does not seem to work...
Mon, 23 Nov 2009 10:04:35 +0100 Cezary Kaliszyk Fixes for recent changes.
Sun, 22 Nov 2009 15:30:23 +0100 Christian Urban updated to Isabelle 22nd November
Sun, 22 Nov 2009 00:01:06 +0100 Christian Urban a little tuning of comments
Sat, 21 Nov 2009 23:23:01 +0100 Christian Urban slight tuning
Sat, 21 Nov 2009 14:45:25 +0100 Christian Urban some debugging code, but cannot find the place where the cprems_of exception is raised
Sat, 21 Nov 2009 14:18:31 +0100 Christian Urban tried to prove the repabs_inj lemma, but failed for the moment
Sat, 21 Nov 2009 13:14:35 +0100 Christian Urban my first version of repabs injection
Sat, 21 Nov 2009 11:16:48 +0100 Christian Urban tuned
Sat, 21 Nov 2009 10:58:08 +0100 Christian Urban tunded
Sat, 21 Nov 2009 03:12:50 +0100 Christian Urban tuned
Sat, 21 Nov 2009 02:53:23 +0100 Christian Urban flagged qenv-stuff as obsolete
Sat, 21 Nov 2009 02:49:39 +0100 Christian Urban simplified get_fun so that it uses directly rty and qty, instead of qenv
Fri, 20 Nov 2009 13:03:01 +0100 Christian Urban started regularize of rtrm/qtrm version; looks quite promising
Thu, 19 Nov 2009 14:17:10 +0100 Christian Urban updated to new Isabelle
Wed, 18 Nov 2009 23:52:48 +0100 Christian Urban fixed the storage of qconst definitions
Fri, 13 Nov 2009 19:32:12 +0100 Cezary Kaliszyk Still don't know how to do the proof automatically.
Fri, 13 Nov 2009 16:44:36 +0100 Christian Urban added some tracing information to all phases of lifting to the function lift_thm
Thu, 12 Nov 2009 13:57:20 +0100 Cezary Kaliszyk merge of the merge?
Thu, 12 Nov 2009 13:56:07 +0100 Cezary Kaliszyk merged
Thu, 12 Nov 2009 12:15:41 +0100 Christian Urban added a FIXME commment
Thu, 12 Nov 2009 12:07:33 +0100 Christian Urban looking up data in quot_info works now (needs qualified string)
Thu, 12 Nov 2009 02:54:40 +0100 Christian Urban changed the quotdata to be a symtab table (needs fixing)
Thu, 12 Nov 2009 02:18:36 +0100 Christian Urban added a container for quotient constants (does not work yet though)
(0) -120 +120 +1000 tip