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
2009-10-28 updated all definitions
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:48:38 +0100] rev 220
updated all definitions
2009-10-28 merged
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:25:36 +0100] rev 219
merged
2009-10-28 added infrastructure for defining lifted constants
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 15:25:11 +0100] rev 218
added infrastructure for defining lifted constants
2009-10-28 First experiments with Lambda
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 14:59:24 +0100] rev 217
First experiments with Lambda
2009-10-28 Fixed mistake in const generation, will postpone this.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 12:22:06 +0100] rev 216
Fixed mistake in const generation, will postpone this.
2009-10-28 More finshed proofs and cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 10:29:00 +0100] rev 215
More finshed proofs and cleaning
2009-10-28 Proof of append_rsp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 28 Oct 2009 10:17:07 +0100] rev 214
Proof of append_rsp
2009-10-28 merged
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 01:49:31 +0100] rev 213
merged
2009-10-28 added a function for matching types
Christian Urban <urbanc@in.tum.de> [Wed, 28 Oct 2009 01:48:45 +0100] rev 212
added a function for matching types
2009-10-27 Manual conversion of equality to equivalence allows lifting append_assoc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 18:05:45 +0100] rev 211
Manual conversion of equality to equivalence allows lifting append_assoc.
2009-10-27 Simplfied interface to repabs_injection.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 18:02:35 +0100] rev 210
Simplfied interface to repabs_injection.
2009-10-27 map_append lifted automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 17:08:47 +0100] rev 209
map_append lifted automatically.
2009-10-27 Manually lifted Map_Append.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 16:15:56 +0100] rev 208
Manually lifted Map_Append.
2009-10-27 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 15:00:15 +0100] rev 207
Merged
2009-10-27 Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 14:59:00 +0100] rev 206
Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.
2009-10-27 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:46:38 +0100] rev 205
tuned
2009-10-27 merged
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:15:40 +0100] rev 204
merged
2009-10-27 added equiv-thm to the quot_info
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 14:14:30 +0100] rev 203
added equiv-thm to the quot_info
2009-10-27 Simplifying FSet with new functions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 12:20:57 +0100] rev 202
Simplifying FSet with new functions.
2009-10-27 added an example about lambda-terms
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:43:02 +0100] rev 201
added an example about lambda-terms
2009-10-27 made quotients compatiple with Nominal; updated keyword file
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:27:53 +0100] rev 200
made quotients compatiple with Nominal; updated keyword file
2009-10-27 merged
Christian Urban <urbanc@in.tum.de> [Tue, 27 Oct 2009 11:03:38 +0100] rev 199
merged
2009-10-27 Completely cleaned Int.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 09:01:12 +0100] rev 198
Completely cleaned Int.
2009-10-27 Further reordering in Int code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 27 Oct 2009 07:46:52 +0100] rev 197
Further reordering in Int code.
2009-10-26 Simplifying Int.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 19:35:30 +0100] rev 196
Simplifying Int.
2009-10-26 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 15:32:17 +0100] rev 195
Merge
2009-10-26 Simplifying Int and Working on map
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 15:31:53 +0100] rev 194
Simplifying Int and Working on map
2009-10-26 merged
Christian Urban <urbanc@in.tum.de> [Mon, 26 Oct 2009 14:18:26 +0100] rev 193
merged
2009-10-26 Simplifying code in int
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 14:16:32 +0100] rev 192
Simplifying code in int
2009-10-26 Symmetry of integer addition
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 13:33:28 +0100] rev 191
Symmetry of integer addition
2009-10-26 Finished the code for adding lower defs, and more things moved to QuotMain
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 11:55:36 +0100] rev 190
Finished the code for adding lower defs, and more things moved to QuotMain
2009-10-26 Making all the definitions from the original ones
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 11:34:02 +0100] rev 189
Making all the definitions from the original ones
2009-10-26 Finished COND_PRS proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 10:20:20 +0100] rev 188
Finished COND_PRS proof.
2009-10-26 Cleaning and fixing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 26 Oct 2009 10:02:50 +0100] rev 187
Cleaning and fixing.
2009-10-26 updated with quotient_def
Christian Urban <urbanc@in.tum.de> [Mon, 26 Oct 2009 02:06:01 +0100] rev 186
updated with quotient_def
2009-10-25 added code for declaring map-functions
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 23:44:41 +0100] rev 185
added code for declaring map-functions
2009-10-24 added "print_quotients" command to th ekeyword file
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 01:31:04 +0200] rev 184
added "print_quotients" command to th ekeyword file
2009-10-24 proved the two lemmas in QuotScript (reformulated them without leading forall)
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 01:15:03 +0200] rev 183
proved the two lemmas in QuotScript (reformulated them without leading forall)
2009-10-24 added data-storage about the quotients
Christian Urban <urbanc@in.tum.de> [Sun, 25 Oct 2009 00:14:40 +0200] rev 182
added data-storage about the quotients
2009-10-24 added another example file about integers (see HOL/Int.thy)
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 22:52:23 +0200] rev 181
added another example file about integers (see HOL/Int.thy)
2009-10-24 changed the definitions of liftet constants to use fun_maps
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 18:17:38 +0200] rev 180
changed the definitions of liftet constants to use fun_maps
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 17:29:20 +0200] rev 179
Merge
2009-10-24 Finally lifted induction, with some manually added simplification lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 17:29:27 +0200] rev 178
Finally lifted induction, with some manually added simplification lemmas.
2009-10-24 changed encoding from utf8 to ISO8 (needed to work with xemacs)
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 16:31:07 +0200] rev 177
changed encoding from utf8 to ISO8 (needed to work with xemacs)
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 16:15:33 +0200] rev 176
Merge
2009-10-24 Preparing infrastructire for LAMBDA_PRS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 16:15:58 +0200] rev 175
Preparing infrastructire for LAMBDA_PRS
2009-10-24 moved the map_funs setup into QuotMain
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 16:09:05 +0200] rev 174
moved the map_funs setup into QuotMain
2009-10-24 Finally completely lift the previously lifted theorems + clean some old stuff
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 14:00:18 +0200] rev 173
Finally completely lift the previously lifted theorems + clean some old stuff
2009-10-24 More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 13:00:54 +0200] rev 172
More infrastructure for automatic lifting of theorems lifted before
2009-10-24 More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 24 Oct 2009 10:16:53 +0200] rev 171
More infrastructure for automatic lifting of theorems lifted before
2009-10-24 Undid wrong merge
cek@localhost.localdomain [Sat, 24 Oct 2009 08:34:14 +0200] rev 170
Undid wrong merge
2009-10-24 Tried rolling back
cek@localhost.localdomain [Sat, 24 Oct 2009 08:29:11 +0200] rev 169
Tried rolling back
2009-10-24 Cleaning the mess
cek@localhost.localdomain [Sat, 24 Oct 2009 08:24:26 +0200] rev 168
Cleaning the mess
2009-10-24 Merge
cek@localhost.localdomain [Sat, 24 Oct 2009 08:09:40 +0200] rev 167
Merge
2009-10-24 Better tactic and simplified the proof further
cek@localhost.localdomain [Sat, 24 Oct 2009 08:09:09 +0200] rev 166
Better tactic and simplified the proof further
2009-10-23 fixed problem with incorrect ABS/REP name
Christian Urban <urbanc@in.tum.de> [Sat, 24 Oct 2009 01:33:29 +0200] rev 165
fixed problem with incorrect ABS/REP name
2009-10-23 Stronger tactic, simpler proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 18:20:06 +0200] rev 164
Stronger tactic, simpler proof.
2009-10-23 Split Finite Set example into separate file
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 16:34:20 +0200] rev 163
Split Finite Set example into separate file
2009-10-23 eqsubst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 16:01:13 +0200] rev 162
eqsubst_tac
2009-10-23 Trying to get a simpler lemma with the whole infrastructure
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 11:24:43 +0200] rev 161
Trying to get a simpler lemma with the whole infrastructure
2009-10-23 Using RANGE tactical allows getting rid of the quotients immediately.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 23 Oct 2009 09:21:45 +0200] rev 160
Using RANGE tactical allows getting rid of the quotients immediately.
2009-10-22 Further developing the tactic and simplifying the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 17:35:40 +0200] rev 159
Further developing the tactic and simplifying the proof
2009-10-22 res_forall_rsp_tac further simplifies the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 16:24:02 +0200] rev 158
res_forall_rsp_tac further simplifies the proof
2009-10-22 Working on the proof and the tactic.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 16:10:06 +0200] rev 157
Working on the proof and the tactic.
2009-10-22 The proof gets simplified
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:45:05 +0200] rev 156
The proof gets simplified
2009-10-22 Removed an assumption
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:44:16 +0200] rev 155
Removed an assumption
2009-10-22 The proof now including manually unfolded higher-order RES_FORALL_RSP.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 15:02:01 +0200] rev 154
The proof now including manually unfolded higher-order RES_FORALL_RSP.
2009-10-22 The problems with 'abs' term.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 13:45:48 +0200] rev 153
The problems with 'abs' term.
2009-10-22 Simplified the proof with some tactic... Still hangs sometimes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 11:43:12 +0200] rev 152
Simplified the proof with some tactic... Still hangs sometimes.
2009-10-22 More proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 10:45:33 +0200] rev 151
More proof
2009-10-22 Got rid of instantiations in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 10:38:00 +0200] rev 150
Got rid of instantiations in the proof
2009-10-22 Removed some debugging messages
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 22 Oct 2009 06:51:27 +0200] rev 149
Removed some debugging messages
2009-10-21 tuned and attempted to store data about the quotients (does not work yet)
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:59:17 +0200] rev 148
tuned and attempted to store data about the quotients (does not work yet)
2009-10-21 tuned
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:16:42 +0200] rev 147
tuned
2009-10-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Thu, 22 Oct 2009 01:15:01 +0200] rev 146
slight tuning
2009-10-21 fixed my_reg
Christian Urban <urbanc@in.tum.de> [Wed, 21 Oct 2009 18:30:42 +0200] rev 145
fixed my_reg
2009-10-21 Reorganization of the construction part
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 16:13:39 +0200] rev 144
Reorganization of the construction part
2009-10-21 Simplified proof more
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 15:01:50 +0200] rev 143
Simplified proof more
2009-10-21 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:30:29 +0200] rev 142
Cleaning the code
2009-10-21 Further reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:15:22 +0200] rev 141
Further reorganization
2009-10-21 Further reorganizing the file
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 14:09:06 +0200] rev 140
Further reorganizing the file
2009-10-21 Reordering
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 13:47:39 +0200] rev 139
Reordering
2009-10-21 cterm_instantiate also fails for some strange reason...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 11:50:53 +0200] rev 138
cterm_instantiate also fails for some strange reason...
2009-10-21 preparing arguments for res_inst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 10:55:32 +0200] rev 137
preparing arguments for res_inst_tac
2009-10-21 Trying res_inst_tac
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 21 Oct 2009 10:30:29 +0200] rev 136
Trying res_inst_tac
2009-10-20 started to write code for storing data about the quotients
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 19:46:22 +0200] rev 135
started to write code for storing data about the quotients
2009-10-20 some minor tuning
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:37:22 +0200] rev 134
some minor tuning
2009-10-20 tuned and fixed the earlier fix
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:31:34 +0200] rev 133
tuned and fixed the earlier fix
2009-10-20 fixed the abs case in my_reg and added an app case
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 09:21:18 +0200] rev 132
fixed the abs case in my_reg and added an app case
2009-10-19 my version of regularise (still needs to be completed)
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 01:17:22 +0200] rev 131
my version of regularise (still needs to be completed)
2009-10-19 moved the map-info and fun-info section to quotient.ML
Christian Urban <urbanc@in.tum.de> [Tue, 20 Oct 2009 00:12:05 +0200] rev 130
moved the map-info and fun-info section to quotient.ML
2009-10-18 Test if we can already do sth with the transformed theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 18 Oct 2009 10:34:53 +0200] rev 129
Test if we can already do sth with the transformed theorem.
2009-10-18 slight fix and tuning
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 08:44:16 +0200] rev 128
slight fix and tuning
2009-10-17 the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
Christian Urban <urbanc@in.tum.de> [Sun, 18 Oct 2009 00:52:10 +0200] rev 127
the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and
2009-10-17 Partial simplification of the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 16:06:54 +0200] rev 126
Partial simplification of the proof
2009-10-17 Some QUOTIENTS
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 15:42:57 +0200] rev 125
Some QUOTIENTS
2009-10-17 Only QUOTIENSs are left to fnish proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 14:16:57 +0200] rev 124
Only QUOTIENSs are left to fnish proof
2009-10-17 More higher order unification problems
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:44:58 +0200] rev 123
More higher order unification problems
2009-10-17 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:48 +0200] rev 122
Merged
2009-10-17 Simplified
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:31:36 +0200] rev 121
Simplified
2009-10-17 Further in the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 12:20:56 +0200] rev 120
Further in the proof
2009-10-17 compose_tac works with the full instantiation.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 11:54:50 +0200] rev 119
compose_tac works with the full instantiation.
2009-10-17 slightly simplified get_fun function
Christian Urban <urbanc@in.tum.de> [Sat, 17 Oct 2009 12:19:06 +0200] rev 118
slightly simplified get_fun function
2009-10-17 The instantiated version is the same modulo beta
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:40:54 +0200] rev 117
The instantiated version is the same modulo beta
2009-10-17 Fully manually instantiated. Still fails...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 10:07:52 +0200] rev 116
Fully manually instantiated. Still fails...
2009-10-17 Little progress with match/instantiate
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 17 Oct 2009 09:04:24 +0200] rev 115
Little progress with match/instantiate
2009-10-16 Fighting with the instantiation
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 19:21:05 +0200] rev 114
Fighting with the instantiation
2009-10-16 Symmetric version of REP_ABS_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 17:05:52 +0200] rev 113
Symmetric version of REP_ABS_RSP
2009-10-16 Progressing with the proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 16:51:01 +0200] rev 112
Progressing with the proof
2009-10-16 Finally fix get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 10:54:31 +0200] rev 111
Finally fix get_fun.
2009-10-16 A fix for one fun_map; doesn't work for more.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 16 Oct 2009 08:48:56 +0200] rev 110
A fix for one fun_map; doesn't work for more.
2009-10-16 fixed the problem with function types; but only type_of works; cterm_of does not work
Christian Urban <urbanc@in.tum.de> [Fri, 16 Oct 2009 03:26:54 +0200] rev 109
fixed the problem with function types; but only type_of works; cterm_of does not work
2009-10-15 Description of the problem with get_fun.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:51:24 +0200] rev 108
Description of the problem with get_fun.
2009-10-15 A proper build_goal_term function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 16:36:20 +0200] rev 107
A proper build_goal_term function.
2009-10-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 12:06:00 +0200] rev 106
Cleaning the code
2009-10-15 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:57:33 +0200] rev 105
Merged
2009-10-15 Cleaning the proofs
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:56:30 +0200] rev 104
Cleaning the proofs
2009-10-15 Cleaning the code, part 4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:55:52 +0200] rev 103
Cleaning the code, part 4
2009-10-15 slightly improved tyRel
Christian Urban <urbanc@in.tum.de> [Thu, 15 Oct 2009 11:53:11 +0200] rev 102
slightly improved tyRel
2009-10-15 Reordering the code, part 3
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:42:14 +0200] rev 101
Reordering the code, part 3
2009-10-15 Reordering the code, part 2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:29:38 +0200] rev 100
Reordering the code, part 2.
2009-10-15 Reordering the code, part 1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:25:25 +0200] rev 99
Reordering the code, part 1.
2009-10-15 Minor cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:20:50 +0200] rev 98
Minor cleaning.
2009-10-15 The definition of Fold1
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 11:17:27 +0200] rev 97
The definition of Fold1
2009-10-15 A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 15 Oct 2009 10:25:23 +0200] rev 96
A number of lemmas for REGULARIZE_TAC and regularizing card1.
2009-10-14 Proving the proper RepAbs version
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 18:13:16 +0200] rev 95
Proving the proper RepAbs version
2009-10-14 Forgot to save, second part of the commit
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:49 +0200] rev 94
Forgot to save, second part of the commit
2009-10-14 Manually regularized list_induct2
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 16:23:32 +0200] rev 93
Manually regularized list_induct2
2009-10-14 Fixed bug in regularise types. Now we can regularise list.induct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 12:05:39 +0200] rev 92
Fixed bug in regularise types. Now we can regularise list.induct.
2009-10-14 Function for checking recursively if lifting is needed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 11:23:55 +0200] rev 91
Function for checking recursively if lifting is needed
2009-10-14 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:50:13 +0200] rev 90
Merge
2009-10-14 Proper handling of non-lifted quantifiers, testing type freezing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 14 Oct 2009 09:47:16 +0200] rev 89
Proper handling of non-lifted quantifiers, testing type freezing.
2009-10-13 slight simplification of atomize_thm
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 22:22:15 +0200] rev 88
slight simplification of atomize_thm
2009-10-13 atomize_thm and meta_quantify.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 18:01:54 +0200] rev 87
atomize_thm and meta_quantify.
2009-10-13 Regularizing HOL all.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 13:37:07 +0200] rev 86
Regularizing HOL all.
2009-10-13 ":" is used for being in a set, "IN" means something else...
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:38:35 +0200] rev 85
":" is used for being in a set, "IN" means something else...
2009-10-13 First (untested) version of regularize for abstractions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 13 Oct 2009 11:03:55 +0200] rev 84
First (untested) version of regularize for abstractions.
2009-10-13 restored old version
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 09:26:19 +0200] rev 83
restored old version
2009-10-12 tuned
Christian Urban <urbanc@in.tum.de> [Tue, 13 Oct 2009 00:02:22 +0200] rev 82
tuned
2009-10-12 slightly modified the parser
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:39:14 +0200] rev 81
slightly modified the parser
2009-10-12 deleted diagnostic code
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:16:20 +0200] rev 80
deleted diagnostic code
2009-10-12 added quotient command (you need to update isar-keywords-prove.el)
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 23:06:14 +0200] rev 79
added quotient command (you need to update isar-keywords-prove.el)
2009-10-12 added new keyword
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 22:44:16 +0200] rev 78
added new keyword
2009-10-12 Bounded quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 16:31:29 +0200] rev 77
Bounded quantifier
2009-10-12 The tyREL function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 15:47:27 +0200] rev 76
The tyREL function.
2009-10-12 started some strange functions
Christian Urban <urbanc@in.tum.de> [Mon, 12 Oct 2009 14:30:50 +0200] rev 75
started some strange functions
2009-10-12 Further with the manual proof
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 12 Oct 2009 13:58:31 +0200] rev 74
Further with the manual proof
2009-10-09 Further experiments with proving induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 17:05:45 +0200] rev 73
Further experiments with proving induction manually
2009-10-09 Testing if I can prove the regularized version of induction manually
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 09 Oct 2009 15:03:43 +0200] rev 72
Testing if I can prove the regularized version of induction manually
2009-10-08 exported parts of QuotMain into a separate ML-file
Christian Urban <urbanc@in.tum.de> [Thu, 08 Oct 2009 14:27:50 +0200] rev 71
exported parts of QuotMain into a separate ML-file
2009-10-06 consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 15:11:30 +0200] rev 70
consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar proof of atomize_eqv.
2009-10-06 simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:56:23 +0200] rev 69
simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)
2009-10-06 renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:41:35 +0200] rev 68
renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)
2009-10-06 tuned; nothing serious
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 11:36:08 +0200] rev 67
tuned; nothing serious
2009-10-06 another improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 09:28:59 +0200] rev 66
another improvement to unlam_def
2009-10-06 one further improvement to unlam_def
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 02:02:51 +0200] rev 65
one further improvement to unlam_def
2009-10-05 simplified the unlam_def function
Christian Urban <urbanc@in.tum.de> [Tue, 06 Oct 2009 01:50:13 +0200] rev 64
simplified the unlam_def function
2009-10-05 added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:54:02 +0200] rev 63
added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)
2009-10-05 used prop_of to get the term of a theorem (replaces crep_thm)
Christian Urban <urbanc@in.tum.de> [Mon, 05 Oct 2009 11:24:32 +0200] rev 62
used prop_of to get the term of a theorem (replaces crep_thm)
2009-10-02 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:10:21 +0200] rev 61
Merged
2009-10-02 First theorem with quantifiers. Learned how to use sledgehammer.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 02 Oct 2009 11:09:33 +0200] rev 60
First theorem with quantifiers. Learned how to use sledgehammer.
2009-10-01 simplified the storage of the map-functions by using TheoryDataFun
Christian Urban <urbanc@in.tum.de> [Thu, 01 Oct 2009 16:10:14 +0200] rev 59
simplified the storage of the map-functions by using TheoryDataFun
2009-09-30 Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 30 Sep 2009 16:57:09 +0200] rev 58
Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.
2009-09-29 used new cong_tac
Christian Urban <urbanc@in.tum.de> [Tue, 29 Sep 2009 22:35:48 +0200] rev 57
used new cong_tac
2009-09-29 First version of handling of the universal quantifier
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 17:46:18 +0200] rev 56
First version of handling of the universal quantifier
2009-09-29 Handling abstraction correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 15:58:14 +0200] rev 55
Handling abstraction correctly.
2009-09-29 second test
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:38:27 +0200] rev 54
second test
2009-09-29 Test line
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 13:24:57 +0200] rev 53
Test line
2009-09-29 Partially fix lifting of card_suc. The quantified variable still needs to be changed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 11:55:37 +0200] rev 52
Partially fix lifting of card_suc. The quantified variable still needs to be changed.
2009-09-29 Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 10:49:31 +0200] rev 51
Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.
2009-09-29 Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:58:02 +0200] rev 50
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.
2009-09-29 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 29 Sep 2009 09:26:22 +0200] rev 49
Merged
2009-09-28 added name to prove
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 23:17:29 +0200] rev 48
added name to prove
2009-09-28 consistent state
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:24:55 +0200] rev 47
consistent state
2009-09-28 some tuning of my code
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 19:22:28 +0200] rev 46
some tuning of my code
2009-09-28 Cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:15:19 +0200] rev 45
Cleanup
2009-09-28 Merged
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 19:10:27 +0200] rev 44
Merged
2009-09-28 Cleaning the code with Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 18:59:04 +0200] rev 43
Cleaning the code with Makarius
2009-09-28 Instnatiation with a schematic variable
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 28 Sep 2009 15:37:38 +0200] rev 42
Instnatiation with a schematic variable
2009-09-28 added ctxt as explicit argument to build_goal; tuned
Christian Urban <urbanc@in.tum.de> [Mon, 28 Sep 2009 02:39:44 +0200] rev 41
added ctxt as explicit argument to build_goal; tuned
2009-09-25 slightly tuned the comment for unlam
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 19:26:18 +0200] rev 40
slightly tuned the comment for unlam
2009-09-25 fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 17:08:50 +0200] rev 39
fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x
2009-09-25 tuned slightly one proof
Christian Urban <urbanc@in.tum.de> [Fri, 25 Sep 2009 16:50:11 +0200] rev 38
tuned slightly one proof
2009-09-25 A version of the tactic that exports variables correctly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 14:50:35 +0200] rev 37
A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.
2009-09-25 Minor cleaning: whitespace, commas etc.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 25 Sep 2009 09:38:16 +0200] rev 36
Minor cleaning: whitespace, commas etc.
2009-09-24 Correctly handling abstractions while building goals
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 17:43:26 +0200] rev 35
Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.
2009-09-24 Minor cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 13:32:52 +0200] rev 34
Minor cleanup
2009-09-24 Found the source for the exception and added a handle for it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 11:38:20 +0200] rev 33
Found the source for the exception and added a handle for it.
2009-09-24 Make the tactic use Trueprop_cong and atomize.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 24 Sep 2009 09:09:46 +0200] rev 32
Make the tactic use Trueprop_cong and atomize.
2009-09-23 Proper code for getting the prop out of the theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:57:56 +0200] rev 31
Proper code for getting the prop out of the theorem.
2009-09-23 Using "atomize" the versions with arbitrary Trueprops can be proven.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 23 Sep 2009 16:44:56 +0200] rev 30
Using "atomize" the versions with arbitrary Trueprops can be proven.
2009-09-22 Proper definition of CARD and some properties of it.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 22 Sep 2009 17:39:52 +0200] rev 29
Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.
2009-09-22 some comments
Christian Urban <urbanc@in.tum.de> [Tue, 22 Sep 2009 09:42:27 +0200] rev 28
some comments
2009-09-21 merged
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:29 +0200] rev 27
merged
2009-09-21 slight tuning
Christian Urban <urbanc@in.tum.de> [Mon, 21 Sep 2009 18:18:01 +0200] rev 26
slight tuning
2009-09-21 The tactic with REPEAT, CHANGED and a proper simpset.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 16:45:44 +0200] rev 25
The tactic with REPEAT, CHANGED and a proper simpset.
2009-09-21 Merged with my changes from the morning:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 21 Sep 2009 10:53:01 +0200] rev 24
Merged with my changes from the morning: further working on the tactic and produced goals.
2009-09-20 some more beautification
Ning@localhost [Sun, 20 Sep 2009 05:48:49 +0100] rev 23
some more beautification
2009-09-20 beautification of some proofs
Ning@localhost [Sun, 20 Sep 2009 05:18:36 +0100] rev 22
beautification of some proofs
2009-09-18 Added more useful quotient facts.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 17:30:33 +0200] rev 21
Added more useful quotient facts.
2009-09-18 Testing the tactic further.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 18 Sep 2009 13:44:06 +0200] rev 20
Testing the tactic further.
2009-09-17 The tactic still only for fset
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 16:55:11 +0200] rev 19
The tactic still only for fset
2009-09-17 Infrastructure for the tactic
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 17 Sep 2009 12:06:06 +0200] rev 18
Infrastructure for the tactic
2009-09-16 More naming/binding suggestions from Makarius
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 16 Sep 2009 11:50:41 +0200] rev 17
More naming/binding suggestions from Makarius
2009-09-15 Code cleanup
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 11:31:35 +0200] rev 16
Code cleanup
2009-09-15 Cleaning the code
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 10:00:34 +0200] rev 15
Cleaning the code
2009-09-15 Generalized interpretation, works for all examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 15 Sep 2009 09:59:56 +0200] rev 14
Generalized interpretation, works for all examples.
2009-08-28 Fixes after suggestions from Makarius:
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 17:12:19 +0200] rev 13
Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling
2009-08-28 More examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 28 Aug 2009 10:01:25 +0200] rev 12
More examples.
2009-08-27 Use metavariables in the 'non-lambda' definitions
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 27 Aug 2009 09:04:39 +0200] rev 11
Use metavariables in the 'non-lambda' definitions
2009-08-26 Make both kinds of definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 26 Aug 2009 11:31:55 +0200] rev 10
Make both kinds of definitions.
2009-08-25 Changed to the use of "modern interface"
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 17:37:50 +0200] rev 9
Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.
2009-08-25 Initial version of the function that builds goals.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 14:37:11 +0200] rev 8
Initial version of the function that builds goals.
2009-08-25 - Build an interpretation for fset from ML level and use it
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 25 Aug 2009 10:35:28 +0200] rev 7
- Build an interpretation for fset from ML level and use it - Added CARD
2009-08-24 added the prove command
Christian Urban <urbanc@in.tum.de> [Tue, 25 Aug 2009 00:30:23 +0200] rev 6
added the prove command
2009-08-21 Fixed
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 21 Aug 2009 13:56:20 +0200] rev 5
Fixed
2009-08-21 tuned
Christian Urban <urbanc@in.tum.de> [Fri, 21 Aug 2009 13:36:58 +0200] rev 4
tuned
2009-08-20 UNION - Append theorem
cek@localhost.localdomain [Thu, 20 Aug 2009 14:44:29 +0200] rev 3
UNION - Append theorem
2009-08-20 update
Christian Urban <urbanc@in.tum.de> [Thu, 20 Aug 2009 10:31:44 +0200] rev 2
update
2009-08-18 updated slightly
Christian Urban <urbanc@in.tum.de> [Tue, 18 Aug 2009 14:04:51 +0200] rev 1
updated slightly
2009-08-11 initial commit
Christian Urban <urbanc@in.tum.de> [Tue, 11 Aug 2009 12:29:15 +0200] rev 0
initial commit
(0) tip