Wed, 04 Nov 2009 13:33:13 +0100 Cezary Kaliszyk Experiments with lifting partially applied constants.
Wed, 04 Nov 2009 12:19:04 +0100 Christian Urban more tuning
Wed, 04 Nov 2009 12:07:22 +0100 Christian Urban slightly tuned
Wed, 04 Nov 2009 11:59:48 +0100 Christian Urban merged
Wed, 04 Nov 2009 11:59:15 +0100 Christian Urban separated the quotient_def into a separate file
Wed, 04 Nov 2009 11:08:05 +0100 Cezary Kaliszyk Experiments in Int
Wed, 04 Nov 2009 10:43:33 +0100 Christian Urban fixed definition of PLUS
Wed, 04 Nov 2009 10:31:20 +0100 Christian Urban simplified the quotient_def code
Wed, 04 Nov 2009 09:52:31 +0100 Cezary Kaliszyk Lifting 'fold1.simps(2)' and some cleaning.
Tue, 03 Nov 2009 18:09:59 +0100 Cezary Kaliszyk Playing with alpha_refl.
Tue, 03 Nov 2009 17:51:10 +0100 Cezary Kaliszyk Alpha.induct now lifts automatically.
Tue, 03 Nov 2009 17:30:43 +0100 Cezary Kaliszyk merge
Tue, 03 Nov 2009 17:30:27 +0100 Cezary Kaliszyk applic_prs
Tue, 03 Nov 2009 16:51:33 +0100 Christian Urban simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Tue, 03 Nov 2009 16:17:19 +0100 Cezary Kaliszyk Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Tue, 03 Nov 2009 14:04:45 +0100 Cezary Kaliszyk merge
Tue, 03 Nov 2009 14:04:21 +0100 Cezary Kaliszyk Preparing infrastructure for general FORALL_PRS
Mon, 02 Nov 2009 18:26:55 +0100 Christian Urban split quotient.ML into two files
Mon, 02 Nov 2009 18:16:19 +0100 Christian Urban slightly saner way of parsing the quotient_def
Mon, 02 Nov 2009 15:39:25 +0100 Christian Urban merged
Mon, 02 Nov 2009 15:38:49 +0100 Christian Urban changed Type.typ_match to Sign.typ_match
Mon, 02 Nov 2009 15:38:03 +0100 Cezary Kaliszyk Fixes after optimization and preparing for a general FORALL_PRS
Mon, 02 Nov 2009 14:57:56 +0100 Cezary Kaliszyk Optimization
Mon, 02 Nov 2009 11:51:50 +0100 Cezary Kaliszyk Map does not fully work yet.
Mon, 02 Nov 2009 11:15:26 +0100 Cezary Kaliszyk Fixed quotdata_lookup.
Mon, 02 Nov 2009 09:47:49 +0100 Christian Urban fixed problem with maps_update
Mon, 02 Nov 2009 09:39:29 +0100 Christian Urban merged
Mon, 02 Nov 2009 09:33:48 +0100 Christian Urban fixed the problem with types in map
Sat, 31 Oct 2009 11:20:55 +0100 Cezary Kaliszyk Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Fri, 30 Oct 2009 19:03:53 +0100 Cezary Kaliszyk Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Fri, 30 Oct 2009 18:31:06 +0100 Cezary Kaliszyk Regularization
Fri, 30 Oct 2009 16:37:09 +0100 Christian Urban merged
Fri, 30 Oct 2009 16:35:43 +0100 Christian Urban added some facts about fresh and support of lam
Fri, 30 Oct 2009 16:24:07 +0100 Cezary Kaliszyk Finally merged the code of the versions of regularize and tested examples.
Fri, 30 Oct 2009 15:52:47 +0100 Cezary Kaliszyk Lemmas about fv.
Fri, 30 Oct 2009 15:35:42 +0100 Christian Urban changed the order of rfv and reformulated a3 with rfv
Fri, 30 Oct 2009 15:32:04 +0100 Christian Urban merged
Fri, 30 Oct 2009 15:30:33 +0100 Christian Urban not sure what changed here
Fri, 30 Oct 2009 15:28:44 +0100 Christian Urban added fv-function
Fri, 30 Oct 2009 15:22:59 +0100 Cezary Kaliszyk The proper real_alpha
Fri, 30 Oct 2009 14:25:37 +0100 Cezary Kaliszyk Finding applications and duplicates filtered out in abstractions
Fri, 30 Oct 2009 12:22:03 +0100 Cezary Kaliszyk Cleaning also in Lam
Fri, 30 Oct 2009 11:25:29 +0100 Cezary Kaliszyk Cleaning of the interface to lift.
Thu, 29 Oct 2009 17:35:03 +0100 Cezary Kaliszyk Tried manually lifting real_alpha
Thu, 29 Oct 2009 13:30:11 +0100 Cezary Kaliszyk More tests in Lam
Thu, 29 Oct 2009 13:29:03 +0100 Cezary Kaliszyk Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
Thu, 29 Oct 2009 12:09:31 +0100 Cezary Kaliszyk Using subst for identity definition.
Thu, 29 Oct 2009 08:46:34 +0100 Cezary Kaliszyk Lifting of the 3 lemmas in LamEx
Thu, 29 Oct 2009 08:06:49 +0100 Cezary Kaliszyk Fixed wrong CARD definition and removed the "Does not work anymore" comment.
Thu, 29 Oct 2009 07:29:12 +0100 Christian Urban merged
Wed, 28 Oct 2009 20:01:20 +0100 Christian Urban updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Wed, 28 Oct 2009 19:46:15 +0100 Christian Urban ported all constant definitions to new scheme
Wed, 28 Oct 2009 19:36:52 +0100 Christian Urban fixed the definition of alpha; this *breaks* some of the experiments
Wed, 28 Oct 2009 18:08:38 +0100 Cezary Kaliszyk disambiguate ===> syntax
Wed, 28 Oct 2009 17:38:37 +0100 Cezary Kaliszyk More cleaning in Lam code
Wed, 28 Oct 2009 17:17:21 +0100 Cezary Kaliszyk cleaned FSet
Wed, 28 Oct 2009 16:48:57 +0100 Cezary Kaliszyk Some cleaning
Wed, 28 Oct 2009 16:16:38 +0100 Cezary Kaliszyk Cleaning the unnecessary theorems in 'IntEx'.
Wed, 28 Oct 2009 16:11:28 +0100 Cezary Kaliszyk Fix also in the general procedure.
Wed, 28 Oct 2009 16:06:19 +0100 Cezary Kaliszyk merge
Wed, 28 Oct 2009 16:05:59 +0100 Cezary Kaliszyk Fixes
Wed, 28 Oct 2009 15:48:38 +0100 Christian Urban updated all definitions
Wed, 28 Oct 2009 15:25:36 +0100 Christian Urban merged
Wed, 28 Oct 2009 15:25:11 +0100 Christian Urban added infrastructure for defining lifted constants
Wed, 28 Oct 2009 14:59:24 +0100 Cezary Kaliszyk First experiments with Lambda
Wed, 28 Oct 2009 12:22:06 +0100 Cezary Kaliszyk Fixed mistake in const generation, will postpone this.
Wed, 28 Oct 2009 10:29:00 +0100 Cezary Kaliszyk More finshed proofs and cleaning
Wed, 28 Oct 2009 10:17:07 +0100 Cezary Kaliszyk Proof of append_rsp
Wed, 28 Oct 2009 01:49:31 +0100 Christian Urban merged
Wed, 28 Oct 2009 01:48:45 +0100 Christian Urban added a function for matching types
Tue, 27 Oct 2009 18:05:45 +0100 Cezary Kaliszyk Manual conversion of equality to equivalence allows lifting append_assoc.
Tue, 27 Oct 2009 18:02:35 +0100 Cezary Kaliszyk Simplfied interface to repabs_injection.
Tue, 27 Oct 2009 17:08:47 +0100 Cezary Kaliszyk map_append lifted automatically.
Tue, 27 Oct 2009 16:15:56 +0100 Cezary Kaliszyk Manually lifted Map_Append.
Tue, 27 Oct 2009 15:00:15 +0100 Cezary Kaliszyk Merged
Tue, 27 Oct 2009 14:59:00 +0100 Cezary Kaliszyk Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
Tue, 27 Oct 2009 14:46:38 +0100 Christian Urban tuned
Tue, 27 Oct 2009 14:15:40 +0100 Christian Urban merged
Tue, 27 Oct 2009 14:14:30 +0100 Christian Urban added equiv-thm to the quot_info
Tue, 27 Oct 2009 12:20:57 +0100 Cezary Kaliszyk Simplifying FSet with new functions.
Tue, 27 Oct 2009 11:43:02 +0100 Christian Urban added an example about lambda-terms
Tue, 27 Oct 2009 11:27:53 +0100 Christian Urban made quotients compatiple with Nominal; updated keyword file
Tue, 27 Oct 2009 11:03:38 +0100 Christian Urban merged
Tue, 27 Oct 2009 09:01:12 +0100 Cezary Kaliszyk Completely cleaned Int.
Tue, 27 Oct 2009 07:46:52 +0100 Cezary Kaliszyk Further reordering in Int code.
Mon, 26 Oct 2009 19:35:30 +0100 Cezary Kaliszyk Simplifying Int.
Mon, 26 Oct 2009 15:32:17 +0100 Cezary Kaliszyk Merge
Mon, 26 Oct 2009 15:31:53 +0100 Cezary Kaliszyk Simplifying Int and Working on map
Mon, 26 Oct 2009 14:18:26 +0100 Christian Urban merged
Mon, 26 Oct 2009 14:16:32 +0100 Cezary Kaliszyk Simplifying code in int
Mon, 26 Oct 2009 13:33:28 +0100 Cezary Kaliszyk Symmetry of integer addition
Mon, 26 Oct 2009 11:55:36 +0100 Cezary Kaliszyk Finished the code for adding lower defs, and more things moved to QuotMain
Mon, 26 Oct 2009 11:34:02 +0100 Cezary Kaliszyk Making all the definitions from the original ones
Mon, 26 Oct 2009 10:20:20 +0100 Cezary Kaliszyk Finished COND_PRS proof.
Mon, 26 Oct 2009 10:02:50 +0100 Cezary Kaliszyk Cleaning and fixing.
Mon, 26 Oct 2009 02:06:01 +0100 Christian Urban updated with quotient_def
Sun, 25 Oct 2009 23:44:41 +0100 Christian Urban added code for declaring map-functions
Sun, 25 Oct 2009 01:31:04 +0200 Christian Urban added "print_quotients" command to th ekeyword file
Sun, 25 Oct 2009 01:15:03 +0200 Christian Urban proved the two lemmas in QuotScript (reformulated them without leading forall)
Sun, 25 Oct 2009 00:14:40 +0200 Christian Urban added data-storage about the quotients
Sat, 24 Oct 2009 22:52:23 +0200 Christian Urban added another example file about integers (see HOL/Int.thy)
Sat, 24 Oct 2009 18:17:38 +0200 Christian Urban changed the definitions of liftet constants to use fun_maps
Sat, 24 Oct 2009 17:29:20 +0200 cek Merge
Sat, 24 Oct 2009 17:29:27 +0200 Cezary Kaliszyk Finally lifted induction, with some manually added simplification lemmas.
Sat, 24 Oct 2009 16:31:07 +0200 Christian Urban changed encoding from utf8 to ISO8 (needed to work with xemacs)
Sat, 24 Oct 2009 16:15:33 +0200 cek Merge
Sat, 24 Oct 2009 16:15:58 +0200 Cezary Kaliszyk Preparing infrastructire for LAMBDA_PRS
Sat, 24 Oct 2009 16:09:05 +0200 Christian Urban moved the map_funs setup into QuotMain
Sat, 24 Oct 2009 14:00:18 +0200 Cezary Kaliszyk Finally completely lift the previously lifted theorems + clean some old stuff
Sat, 24 Oct 2009 13:00:54 +0200 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
Sat, 24 Oct 2009 10:16:53 +0200 Cezary Kaliszyk More infrastructure for automatic lifting of theorems lifted before
Sat, 24 Oct 2009 08:34:14 +0200 cek Undid wrong merge
Sat, 24 Oct 2009 08:29:11 +0200 cek Tried rolling back
Sat, 24 Oct 2009 08:24:26 +0200 cek Cleaning the mess
Sat, 24 Oct 2009 08:09:40 +0200 cek Merge
Sat, 24 Oct 2009 08:09:09 +0200 cek Better tactic and simplified the proof further
Sat, 24 Oct 2009 01:33:29 +0200 Christian Urban fixed problem with incorrect ABS/REP name
Fri, 23 Oct 2009 18:20:06 +0200 Cezary Kaliszyk Stronger tactic, simpler proof.
Fri, 23 Oct 2009 16:34:20 +0200 Cezary Kaliszyk Split Finite Set example into separate file
Fri, 23 Oct 2009 16:01:13 +0200 Cezary Kaliszyk eqsubst_tac
(0) -120 +120 +1000 tip