2009-11-30 added facilities to get all stored quotient data (equiv thms etc)
Christian Urban <urbanc@in.tum.de> [Mon, 30 Nov 2009 12:26:08 +0100] rev 460
added facilities to get all stored quotient data (equiv thms etc)
2009-11-30 More code cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Nov 2009 12:14:20 +0100] rev 459
More code cleaning
2009-11-30 Code cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Nov 2009 11:53:20 +0100] rev 458
Code cleaning.
2009-11-30 Commented clean-tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Nov 2009 10:16:10 +0100] rev 457
Commented clean-tac
2009-11-30 Added another induction to LFex
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 30 Nov 2009 02:05:22 +0100] rev 456
Added another induction to LFex
2009-11-29 tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de> [Sun, 29 Nov 2009 23:59:37 +0100] rev 455
tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29 added a new version of QuotMain to experiment with qids
Christian Urban <urbanc@in.tum.de> [Sun, 29 Nov 2009 19:48:55 +0100] rev 454
added a new version of QuotMain to experiment with qids
2009-11-29 started functions for qid-insertion and fixed a bug in regularise
Christian Urban <urbanc@in.tum.de> [Sun, 29 Nov 2009 17:47:37 +0100] rev 453
started functions for qid-insertion and fixed a bug in regularise
2009-11-29 Removed unnecessary HOL_ss which proved one of the subgoals.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 29 Nov 2009 09:38:07 +0100] rev 452
Removed unnecessary HOL_ss which proved one of the subgoals.
2009-11-29 Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 29 Nov 2009 08:48:06 +0100] rev 451
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
2009-11-29 introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de> [Sun, 29 Nov 2009 03:59:18 +0100] rev 450
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-29 tuned
Christian Urban <urbanc@in.tum.de> [Sun, 29 Nov 2009 02:51:42 +0100] rev 449
tuned
2009-11-28 improved pattern matching inside the inj_repabs_tacs
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 19:14:12 +0100] rev 448
improved pattern matching inside the inj_repabs_tacs
2009-11-28 selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 18:49:39 +0100] rev 447
selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
2009-11-28 removed old inj_repabs_tac; kept only the one with (selective) debugging information
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:45:22 +0100] rev 446
removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28 renamed r_mk_comb_tac to inj_repabs_tac
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:33:04 +0100] rev 445
renamed r_mk_comb_tac to inj_repabs_tac
2009-11-28 tuning
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:15:05 +0100] rev 444
tuning
2009-11-28 tuned comments
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 14:03:01 +0100] rev 443
tuned comments
2009-11-28 renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 13:54:48 +0100] rev 442
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
2009-11-28 Manually finished LF induction.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 08:46:24 +0100] rev 441
Manually finished LF induction.
2009-11-28 Moved fast instantiation to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 08:04:23 +0100] rev 440
Moved fast instantiation to QuotMain
2009-11-28 LFex proof a bit further.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 07:44:17 +0100] rev 439
LFex proof a bit further.
2009-11-28 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 06:15:06 +0100] rev 438
merge
2009-11-28 Looking at repabs proof in LF.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 06:14:50 +0100] rev 437
Looking at repabs proof in LF.
2009-11-28 further proper merge
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 05:53:31 +0100] rev 436
further proper merge
2009-11-28 merged
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 05:49:16 +0100] rev 435
merged
2009-11-28 more simplification
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 05:47:13 +0100] rev 434
more simplification
2009-11-28 Merged and tested that all works.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 05:43:18 +0100] rev 433
Merged and tested that all works.
2009-11-28 Finished and tested the new regularize
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 05:29:30 +0100] rev 432
Finished and tested the new regularize
2009-11-28 more tuning of the repabs-tactics
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 05:09:22 +0100] rev 431
more tuning of the repabs-tactics
2009-11-28 fixed examples in IntEx and FSet
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 04:46:03 +0100] rev 430
fixed examples in IntEx and FSet
2009-11-28 merged
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 04:37:30 +0100] rev 429
merged
2009-11-28 fixed previous commit
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 04:37:04 +0100] rev 428
fixed previous commit
2009-11-28 Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 04:02:54 +0100] rev 427
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
2009-11-28 Merged comment
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 03:17:22 +0100] rev 426
Merged comment
2009-11-28 Integrated Stefan's tactic and changed substs to simps with empty context.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 28 Nov 2009 03:07:38 +0100] rev 425
Integrated Stefan's tactic and changed substs to simps with empty context.
2009-11-28 some slight tuning of the apply-tactic
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 03:06:22 +0100] rev 424
some slight tuning of the apply-tactic
2009-11-28 annotated a proof with all steps and simplified LAMBDA_RES_TAC
Christian Urban <urbanc@in.tum.de> [Sat, 28 Nov 2009 02:54:24 +0100] rev 423
annotated a proof with all steps and simplified LAMBDA_RES_TAC
2009-11-27 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 18:38:44 +0100] rev 422
Merge
2009-11-27 The magical code from Stefan, will need to be integrated in the Simproc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 18:38:09 +0100] rev 421
The magical code from Stefan, will need to be integrated in the Simproc.
2009-11-27 replaced FIRST' (map rtac list) with resolve_tac list
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 13:59:52 +0100] rev 420
replaced FIRST' (map rtac list) with resolve_tac list
2009-11-27 Simplifying arguments; got rid of trans2_thm.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 10:04:49 +0100] rev 419
Simplifying arguments; got rid of trans2_thm.
2009-11-27 Cleaning of LFex. Lambda_prs fails to unify in 2 places.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 09:16:32 +0100] rev 418
Cleaning of LFex. Lambda_prs fails to unify in 2 places.
2009-11-27 Recommit
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 08:22:46 +0100] rev 417
Recommit
2009-11-27 Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 08:15:23 +0100] rev 416
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
2009-11-27 More cleaning in QuotMain, identity handling.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 07:16:16 +0100] rev 415
More cleaning in QuotMain, identity handling.
2009-11-27 Minor cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 27 Nov 2009 07:00:14 +0100] rev 414
Minor cleaning
2009-11-27 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 04:02:20 +0100] rev 413
tuned
2009-11-27 some tuning
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 03:56:18 +0100] rev 412
some tuning
2009-11-27 simplified gen_frees_tac and properly named abstracted variables
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 03:33:30 +0100] rev 411
simplified gen_frees_tac and properly named abstracted variables
2009-11-27 removed CHANGED'
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:58:28 +0100] rev 410
removed CHANGED'
2009-11-27 introduced a separate lemma for id_simps
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:55:56 +0100] rev 409
introduced a separate lemma for id_simps
2009-11-27 renamed inj_REPABS to inj_repabs_trm
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:45:54 +0100] rev 408
renamed inj_REPABS to inj_repabs_trm
2009-11-27 tuned comments and moved slightly some code
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:44:11 +0100] rev 407
tuned comments and moved slightly some code
2009-11-27 deleted obsolete qenv code
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:35:50 +0100] rev 406
deleted obsolete qenv code
2009-11-27 renamed REGULARIZE to be regularize
Christian Urban <urbanc@in.tum.de> [Fri, 27 Nov 2009 02:23:49 +0100] rev 405
renamed REGULARIZE to be regularize
2009-11-26 more tuning
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 21:16:59 +0100] rev 404
more tuning
2009-11-26 deleted get_fun_old and stuff
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 21:04:17 +0100] rev 403
deleted get_fun_old and stuff
2009-11-26 recommited changes of comments
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 21:01:53 +0100] rev 402
recommited changes of comments
2009-11-26 Merge Again
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 26 Nov 2009 20:32:56 +0100] rev 401
Merge Again
2009-11-26 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 26 Nov 2009 20:32:33 +0100] rev 400
Merged
2009-11-26 tuned comments
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 20:18:36 +0100] rev 399
tuned comments
2009-11-26 some diagnostic code for r_mk_comb
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 19:51:31 +0100] rev 398
some diagnostic code for r_mk_comb
2009-11-26 introduced a new property for Ball and ===> on the left
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 16:23:24 +0100] rev 397
introduced a new property for Ball and ===> on the left
2009-11-26 fixed QuotList
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 13:52:46 +0100] rev 396
fixed QuotList
2009-11-26 changed left-res
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 13:46:00 +0100] rev 395
changed left-res
2009-11-26 Manually regularized akind_aty_atrm.induct
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 26 Nov 2009 12:21:47 +0100] rev 394
Manually regularized akind_aty_atrm.induct
2009-11-26 Playing with Monos in LFex.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 26 Nov 2009 10:52:24 +0100] rev 393
Playing with Monos in LFex.
2009-11-26 Fixed FSet after merge.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 26 Nov 2009 10:32:31 +0100] rev 392
Fixed FSet after merge.
2009-11-26 merged
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 03:18:38 +0100] rev 391
merged
2009-11-26 test with monos
Christian Urban <urbanc@in.tum.de> [Thu, 26 Nov 2009 02:31:00 +0100] rev 390
test with monos
2009-11-25 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 21:48:32 +0100] rev 389
applic_prs
2009-11-25 polishing
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 15:43:12 +0100] rev 388
polishing
2009-11-25 reordered the code
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 15:20:10 +0100] rev 387
reordered the code
2009-11-25 Moved exception handling to QuotMain and cleaned FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 14:25:29 +0100] rev 386
Moved exception handling to QuotMain and cleaned FSet.
2009-11-25 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 14:16:33 +0100] rev 385
Merge
2009-11-25 Finished manual lifting of list_induct_part :)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 14:15:34 +0100] rev 384
Finished manual lifting of list_induct_part :)
2009-11-25 comments tuning and slight reordering
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 12:27:28 +0100] rev 383
comments tuning and slight reordering
2009-11-25 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 11:59:49 +0100] rev 382
Merge
2009-11-25 More moving from QuotMain to UnusedQuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 11:58:56 +0100] rev 381
More moving from QuotMain to UnusedQuotMain
2009-11-25 deleted some obsolete diagnostic code
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 11:46:59 +0100] rev 380
deleted some obsolete diagnostic code
2009-11-25 Removed unused things from QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 11:41:42 +0100] rev 379
Removed unused things from QuotMain.
2009-11-25 All examples work again.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 10:52:21 +0100] rev 378
All examples work again.
2009-11-25 cleaning in MyInt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 10:39:53 +0100] rev 377
cleaning in MyInt
2009-11-25 lambda_prs and cleaning the existing examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 25 Nov 2009 10:34:03 +0100] rev 376
lambda_prs and cleaning the existing examples.
2009-11-25 merged
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 03:47:07 +0100] rev 375
merged
2009-11-25 fixed the problem with generalising variables; at the moment it is quite a hack
Christian Urban <urbanc@in.tum.de> [Wed, 25 Nov 2009 03:45:44 +0100] rev 374
fixed the problem with generalising variables; at the moment it is quite a hack
2009-11-24 Ho-matching failures...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 20:13:16 +0100] rev 373
Ho-matching failures...
2009-11-24 changed unification to matching
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 19:09:29 +0100] rev 372
changed unification to matching
2009-11-24 unification
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 18:13:57 +0100] rev 371
unification
2009-11-24 Lambda & SOLVED' for new quotient_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 18:13:18 +0100] rev 370
Lambda & SOLVED' for new quotient_tac
2009-11-24 merged
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 17:35:31 +0100] rev 369
merged
2009-11-24 Conversion
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 17:00:53 +0100] rev 368
Conversion
2009-11-24 The non-working procedure_tac.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 16:20:34 +0100] rev 367
The non-working procedure_tac.
2009-11-24 merged
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 16:10:31 +0100] rev 366
merged
2009-11-24 use error instead of raising our own exception
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 15:31:29 +0100] rev 365
use error instead of raising our own exception
2009-11-24 Fixes to the tactic after quotient_tac changed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 15:18:00 +0100] rev 364
Fixes to the tactic after quotient_tac changed.
2009-11-24 merged
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 15:15:33 +0100] rev 363
merged
2009-11-24 added a prepare_tac
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 15:15:10 +0100] rev 362
added a prepare_tac
2009-11-24 TRY' for clean_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 14:41:47 +0100] rev 361
TRY' for clean_tac
2009-11-24 Moved cleaning to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 14:19:54 +0100] rev 360
Moved cleaning to QuotMain
2009-11-24 New cleaning tactic
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 14:16:57 +0100] rev 359
New cleaning tactic
2009-11-24 explicit phases for the cleaning
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 13:46:36 +0100] rev 358
explicit phases for the cleaning
2009-11-24 Separate regularize_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 12:25:04 +0100] rev 357
Separate regularize_tac
2009-11-24 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.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 08:36:28 +0100] rev 356
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.
2009-11-24 More fixes for inj_REPABS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 24 Nov 2009 08:35:04 +0100] rev 355
More fixes for inj_REPABS
2009-11-24 addded a tactic, which sets up the three goals of the `algorithm'
Christian Urban <urbanc@in.tum.de> [Tue, 24 Nov 2009 01:36:50 +0100] rev 354
addded a tactic, which sets up the three goals of the `algorithm'
2009-11-23 fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 23:09:03 +0100] rev 353
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
2009-11-23 merged
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 22:00:54 +0100] rev 352
merged
2009-11-23 tuned some comments
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 21:59:57 +0100] rev 351
tuned some comments
2009-11-23 Another not-typechecking regularized term.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 21:56:30 +0100] rev 350
Another not-typechecking regularized term.
2009-11-23 domain_type in regularizing equality
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 21:48:44 +0100] rev 349
domain_type in regularizing equality
2009-11-23 More theorems lifted in the goal-directed way.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 21:12:16 +0100] rev 348
More theorems lifted in the goal-directed way.
2009-11-23 Finished temporary goal-directed lift_theorem wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 20:10:39 +0100] rev 347
Finished temporary goal-directed lift_theorem wrapper.
2009-11-23 merged
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 16:13:19 +0100] rev 346
merged
2009-11-23 a version of inj_REPABS (needs to be looked at again later)
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 16:12:50 +0100] rev 345
a version of inj_REPABS (needs to be looked at again later)
2009-11-23 Fixes for atomize
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 15:47:14 +0100] rev 344
Fixes for atomize
2009-11-23 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 15:08:25 +0100] rev 343
merge
2009-11-23 lift_thm with a goal.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 15:08:09 +0100] rev 342
lift_thm with a goal.
2009-11-23 slight change in code layout
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 15:02:48 +0100] rev 341
slight change in code layout
2009-11-23 Fixes for new code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 14:40:53 +0100] rev 340
Fixes for new code
2009-11-23 Removing dead code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 14:32:11 +0100] rev 339
Removing dead code
2009-11-23 Move atomize_goal to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 14:16:41 +0100] rev 338
Move atomize_goal to QuotMain
2009-11-23 Removed second implementation of Regularize/Inject from FSet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 14:05:02 +0100] rev 337
Removed second implementation of Regularize/Inject from FSet.
2009-11-23 Moved new repabs_inj code to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 13:55:31 +0100] rev 336
Moved new repabs_inj code to QuotMain
2009-11-23 New repabs behaves the same way as old one.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 13:46:14 +0100] rev 335
New repabs behaves the same way as old one.
2009-11-23 code review with Cezary
Christian Urban <urbanc@in.tum.de> [Mon, 23 Nov 2009 13:24:12 +0100] rev 334
code review with Cezary
2009-11-23 The other branch does not seem to work...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 10:26:59 +0100] rev 333
The other branch does not seem to work...
2009-11-23 Fixes for recent changes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 23 Nov 2009 10:04:35 +0100] rev 332
Fixes for recent changes.
2009-11-22 updated to Isabelle 22nd November
Christian Urban <urbanc@in.tum.de> [Sun, 22 Nov 2009 15:30:23 +0100] rev 331
updated to Isabelle 22nd November
2009-11-21 a little tuning of comments
Christian Urban <urbanc@in.tum.de> [Sun, 22 Nov 2009 00:01:06 +0100] rev 330
a little tuning of comments
2009-11-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 23:23:01 +0100] rev 329
slight tuning
2009-11-21 some debugging code, but cannot find the place where the cprems_of exception is raised
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 14:45:25 +0100] rev 328
some debugging code, but cannot find the place where the cprems_of exception is raised
2009-11-21 tried to prove the repabs_inj lemma, but failed for the moment
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 14:18:31 +0100] rev 327
tried to prove the repabs_inj lemma, but failed for the moment
2009-11-21 my first version of repabs injection
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 13:14:35 +0100] rev 326
my first version of repabs injection
2009-11-21 tuned
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 11:16:48 +0100] rev 325
tuned
2009-11-21 tunded
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 10:58:08 +0100] rev 324
tunded
2009-11-21 tuned
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 03:12:50 +0100] rev 323
tuned
2009-11-21 flagged qenv-stuff as obsolete
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 02:53:23 +0100] rev 322
flagged qenv-stuff as obsolete
2009-11-21 simplified get_fun so that it uses directly rty and qty, instead of qenv
Christian Urban <urbanc@in.tum.de> [Sat, 21 Nov 2009 02:49:39 +0100] rev 321
simplified get_fun so that it uses directly rty and qty, instead of qenv
2009-11-20 started regularize of rtrm/qtrm version; looks quite promising
Christian Urban <urbanc@in.tum.de> [Fri, 20 Nov 2009 13:03:01 +0100] rev 320
started regularize of rtrm/qtrm version; looks quite promising
2009-11-19 updated to new Isabelle
Christian Urban <urbanc@in.tum.de> [Thu, 19 Nov 2009 14:17:10 +0100] rev 319
updated to new Isabelle
2009-11-18 fixed the storage of qconst definitions
Christian Urban <urbanc@in.tum.de> [Wed, 18 Nov 2009 23:52:48 +0100] rev 318
fixed the storage of qconst definitions
2009-11-13 Still don't know how to do the proof automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 13 Nov 2009 19:32:12 +0100] rev 317
Still don't know how to do the proof automatically.
2009-11-13 added some tracing information to all phases of lifting to the function lift_thm
Christian Urban <urbanc@in.tum.de> [Fri, 13 Nov 2009 16:44:36 +0100] rev 316
added some tracing information to all phases of lifting to the function lift_thm
2009-11-12 merge of the merge?
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 12 Nov 2009 13:57:20 +0100] rev 315
merge of the merge?
2009-11-12 merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 12 Nov 2009 13:56:07 +0100] rev 314
merged
2009-11-12 added a FIXME commment
Christian Urban <urbanc@in.tum.de> [Thu, 12 Nov 2009 12:15:41 +0100] rev 313
added a FIXME commment
2009-11-12 looking up data in quot_info works now (needs qualified string)
Christian Urban <urbanc@in.tum.de> [Thu, 12 Nov 2009 12:07:33 +0100] rev 312
looking up data in quot_info works now (needs qualified string)
2009-11-12 changed the quotdata to be a symtab table (needs fixing)
Christian Urban <urbanc@in.tum.de> [Thu, 12 Nov 2009 02:54:40 +0100] rev 311
changed the quotdata to be a symtab table (needs fixing)
2009-11-12 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de> [Thu, 12 Nov 2009 02:18:36 +0100] rev 310
added a container for quotient constants (does not work yet though)
2009-11-11 Lifting towards goal and manually finished the proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 11 Nov 2009 22:30:43 +0100] rev 309
Lifting towards goal and manually finished the proof.
2009-11-11 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 11 Nov 2009 18:51:59 +0100] rev 308
merge
2009-11-11 Modifications while preparing the goal-directed version.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 11 Nov 2009 18:49:46 +0100] rev 307
Modifications while preparing the goal-directed version.
2009-11-11 updated to new Theory_Data and to new Isabelle
Christian Urban <urbanc@in.tum.de> [Wed, 11 Nov 2009 11:59:22 +0100] rev 306
updated to new Theory_Data and to new Isabelle
2009-11-11 Removed 'Toplevel.program' for polyml 5.3
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 11 Nov 2009 10:22:47 +0100] rev 305
Removed 'Toplevel.program' for polyml 5.3
2009-11-10 Atomizing a "goal" theorems.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 10 Nov 2009 17:43:05 +0100] rev 304
Atomizing a "goal" theorems.
2009-11-10 More code cleaning and commenting
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 10 Nov 2009 09:32:16 +0100] rev 303
More code cleaning and commenting
2009-11-09 Minor cleaning and removing of some 'handle _'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 09 Nov 2009 15:40:43 +0100] rev 302
Minor cleaning and removing of some 'handle _'.
2009-11-09 Cleaning and commenting
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 09 Nov 2009 15:23:33 +0100] rev 301
Cleaning and commenting
2009-11-09 Fixes for the other get_fun implementation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 09 Nov 2009 13:47:46 +0100] rev 300
Fixes for the other get_fun implementation.
2009-11-06 permutation lifting works now also
Christian Urban <urbanc@in.tum.de> [Fri, 06 Nov 2009 19:43:09 +0100] rev 299
permutation lifting works now also
2009-11-06 merged
Christian Urban <urbanc@in.tum.de> [Fri, 06 Nov 2009 19:26:32 +0100] rev 298
merged
2009-11-06 updated to new Isabelle version and added a new example file
Christian Urban <urbanc@in.tum.de> [Fri, 06 Nov 2009 19:26:08 +0100] rev 297
updated to new Isabelle version and added a new example file
2009-11-06 Minor changes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 06 Nov 2009 17:42:20 +0100] rev 296
Minor changes
2009-11-06 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 06 Nov 2009 11:02:11 +0100] rev 295
merge
2009-11-06 fold_rsp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 06 Nov 2009 11:01:22 +0100] rev 294
fold_rsp
2009-11-06 tuned the code in quotient and quotient_def
Christian Urban <urbanc@in.tum.de> [Fri, 06 Nov 2009 09:48:37 +0100] rev 293
tuned the code in quotient and quotient_def
2009-11-05 More functionality for lifting list.cases and list.recs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 05 Nov 2009 16:43:57 +0100] rev 292
More functionality for lifting list.cases and list.recs.
2009-11-05 merged
Christian Urban <urbanc@in.tum.de> [Thu, 05 Nov 2009 13:47:41 +0100] rev 291
merged
2009-11-05 removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de> [Thu, 05 Nov 2009 13:47:04 +0100] rev 290
removed typing information from get_fun in quotient_def; *potentially* dangerous
2009-11-05 Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 05 Nov 2009 13:36:46 +0100] rev 289
Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
2009-11-05 removed Simplifier.context
Christian Urban <urbanc@in.tum.de> [Thu, 05 Nov 2009 10:46:54 +0100] rev 288
removed Simplifier.context
2009-11-05 replaced check_term o parse_term by read_term
Christian Urban <urbanc@in.tum.de> [Thu, 05 Nov 2009 10:23:27 +0100] rev 287
replaced check_term o parse_term by read_term
2009-11-05 merged
Christian Urban <urbanc@in.tum.de> [Thu, 05 Nov 2009 09:55:21 +0100] rev 286
merged
2009-11-05 Infrastructure for polymorphic types
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 05 Nov 2009 09:38:34 +0100] rev 285
Infrastructure for polymorphic types
2009-11-04 Two new tests for get_fun. Second one fails.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 16:10:39 +0100] rev 284
Two new tests for get_fun. Second one fails.
2009-11-04 Type instantiation in regularize
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 15:27:32 +0100] rev 283
Type instantiation in regularize
2009-11-04 Description of regularize
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 14:03:46 +0100] rev 282
Description of regularize
2009-11-04 Experiments with lifting partially applied constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 13:33:13 +0100] rev 281
Experiments with lifting partially applied constants.
2009-11-04 more tuning
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 12:19:04 +0100] rev 280
more tuning
2009-11-04 slightly tuned
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 12:07:22 +0100] rev 279
slightly tuned
2009-11-04 merged
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 11:59:48 +0100] rev 278
merged
2009-11-04 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 11:59:15 +0100] rev 277
separated the quotient_def into a separate file
2009-11-04 Experiments in Int
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 11:08:05 +0100] rev 276
Experiments in Int
2009-11-04 fixed definition of PLUS
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 10:43:33 +0100] rev 275
fixed definition of PLUS
2009-11-04 simplified the quotient_def code
Christian Urban <urbanc@in.tum.de> [Wed, 04 Nov 2009 10:31:20 +0100] rev 274
simplified the quotient_def code
2009-11-04 Lifting 'fold1.simps(2)' and some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 04 Nov 2009 09:52:31 +0100] rev 273
Lifting 'fold1.simps(2)' and some cleaning.
2009-11-03 Playing with alpha_refl.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 18:09:59 +0100] rev 272
Playing with alpha_refl.
2009-11-03 Alpha.induct now lifts automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:51:10 +0100] rev 271
Alpha.induct now lifts automatically.
2009-11-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:30:43 +0100] rev 270
merge
2009-11-03 applic_prs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 17:30:27 +0100] rev 269
applic_prs
2009-11-03 simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de> [Tue, 03 Nov 2009 16:51:33 +0100] rev 268
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
2009-11-03 Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 16:17:19 +0100] rev 267
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
2009-11-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 14:04:45 +0100] rev 266
merge
2009-11-03 Preparing infrastructure for general FORALL_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 03 Nov 2009 14:04:21 +0100] rev 265
Preparing infrastructure for general FORALL_PRS
2009-11-02 split quotient.ML into two files
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 18:26:55 +0100] rev 264
split quotient.ML into two files
2009-11-02 slightly saner way of parsing the quotient_def
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 18:16:19 +0100] rev 263
slightly saner way of parsing the quotient_def
2009-11-02 merged
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 15:39:25 +0100] rev 262
merged
2009-11-02 changed Type.typ_match to Sign.typ_match
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 15:38:49 +0100] rev 261
changed Type.typ_match to Sign.typ_match
2009-11-02 Fixes after optimization and preparing for a general FORALL_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 15:38:03 +0100] rev 260
Fixes after optimization and preparing for a general FORALL_PRS
2009-11-02 Optimization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 14:57:56 +0100] rev 259
Optimization
2009-11-02 Map does not fully work yet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 11:51:50 +0100] rev 258
Map does not fully work yet.
2009-11-02 Fixed quotdata_lookup.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 02 Nov 2009 11:15:26 +0100] rev 257
Fixed quotdata_lookup.
2009-11-02 fixed problem with maps_update
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:47:49 +0100] rev 256
fixed problem with maps_update
2009-11-02 merged
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:39:29 +0100] rev 255
merged
2009-11-02 fixed the problem with types in map
Christian Urban <urbanc@in.tum.de> [Mon, 02 Nov 2009 09:33:48 +0100] rev 254
fixed the problem with types in map
2009-10-31 Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 31 Oct 2009 11:20:55 +0100] rev 253
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
2009-10-30 Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 19:03:53 +0100] rev 252
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
2009-10-30 Regularization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 18:31:06 +0100] rev 251
Regularization
2009-10-30 merged
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 16:37:09 +0100] rev 250
merged
2009-10-30 added some facts about fresh and support of lam
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 16:35:43 +0100] rev 249
added some facts about fresh and support of lam
2009-10-30 Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 16:24:07 +0100] rev 248
Finally merged the code of the versions of regularize and tested examples.
2009-10-30 Lemmas about fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 15:52:47 +0100] rev 247
Lemmas about fv.
2009-10-30 changed the order of rfv and reformulated a3 with rfv
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:35:42 +0100] rev 246
changed the order of rfv and reformulated a3 with rfv
2009-10-30 merged
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:32:04 +0100] rev 245
merged
2009-10-30 not sure what changed here
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:30:33 +0100] rev 244
not sure what changed here
2009-10-30 added fv-function
Christian Urban <urbanc@in.tum.de> [Fri, 30 Oct 2009 15:28:44 +0100] rev 243
added fv-function
2009-10-30 The proper real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 15:22:59 +0100] rev 242
The proper real_alpha
2009-10-30 Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 14:25:37 +0100] rev 241
Finding applications and duplicates filtered out in abstractions
2009-10-30 Cleaning also in Lam
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 12:22:03 +0100] rev 240
Cleaning also in Lam
2009-10-30 Cleaning of the interface to lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 30 Oct 2009 11:25:29 +0100] rev 239
Cleaning of the interface to lift.
2009-10-29 Tried manually lifting real_alpha
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 17:35:03 +0100] rev 238
Tried manually lifting real_alpha
2009-10-29 More tests in Lam
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 13:30:11 +0100] rev 237
More tests in Lam
2009-10-29 Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 13:29:03 +0100] rev 236
Cleaning of 'map id' and 'prod_fun id id' in lower_defs.
2009-10-29 Using subst for identity definition.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 12:09:31 +0100] rev 235
Using subst for identity definition.
2009-10-29 Lifting of the 3 lemmas in LamEx
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 08:46:34 +0100] rev 234
Lifting of the 3 lemmas in LamEx
2009-10-29 Fixed wrong CARD definition and removed the "Does not work anymore" comment.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 29 Oct 2009 08:06:49 +0100] rev 233
Fixed wrong CARD definition and removed the "Does not work anymore" comment.
2009-10-29 merged
Christian Urban <urbanc@in.tum.de> [Thu, 29 Oct 2009 07:29:12 +0100] rev 232
merged
2009-10-28 updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 20:01:20 +0100] rev 231
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
2009-10-28 ported all constant definitions to new scheme
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 19:46:15 +0100] rev 230
ported all constant definitions to new scheme
2009-10-28 fixed the definition of alpha; this *breaks* some of the experiments
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 19:36:52 +0100] rev 229
fixed the definition of alpha; this *breaks* some of the experiments
2009-10-28 disambiguate ===> syntax
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 18:08:38 +0100] rev 228
disambiguate ===> syntax
2009-10-28 More cleaning in Lam code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 17:38:37 +0100] rev 227
More cleaning in Lam code
2009-10-28 cleaned FSet
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 17:17:21 +0100] rev 226
cleaned FSet
2009-10-28 Some cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:48:57 +0100] rev 225
Some cleaning
2009-10-28 Cleaning the unnecessary theorems in 'IntEx'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:16:38 +0100] rev 224
Cleaning the unnecessary theorems in 'IntEx'.
2009-10-28 Fix also in the general procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:11:28 +0100] rev 223
Fix also in the general procedure.
2009-10-28 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:06:19 +0100] rev 222
merge
2009-10-28 Fixes
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 16:05:59 +0100] rev 221
Fixes
(0) -240 +240 +1000 tip