2010-03-08 Update the comments
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:33:55 +0100] rev 1358
Update the comments
2010-03-08 Gather bindings with same binder, and generate only one permutation for them.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 10:08:31 +0100] rev 1357
Gather bindings with same binder, and generate only one permutation for them.
2010-03-08 Undo effects of simp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 08 Mar 2010 02:40:16 +0100] rev 1356
Undo effects of simp.
2010-03-07 merged
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:57 +0100] rev 1355
merged
2010-03-07 updated to renamings in Isabelle
Christian Urban <urbanc@in.tum.de> [Sun, 07 Mar 2010 21:30:12 +0100] rev 1354
updated to renamings in Isabelle
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:56:58 +0100] rev 1353
merged
2010-03-04 merged
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:34 +0100] rev 1352
merged
2010-03-04 more proofs in Abs and work on Core Haskell
Christian Urban <urbanc@in.tum.de> [Thu, 04 Mar 2010 15:31:21 +0100] rev 1351
more proofs in Abs and work on Core Haskell
2010-03-03 added a lemma that permutations can be represented as sums of swapping
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 19:10:40 +0100] rev 1350
added a lemma that permutations can be represented as sums of swapping
2010-03-05 Still unable to show supp=fv for let with one existential.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 18:14:04 +0100] rev 1349
Still unable to show supp=fv for let with one existential.
2010-03-05 Ported LF to the parser interface.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 17:09:48 +0100] rev 1348
Ported LF to the parser interface.
2010-03-05 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:56:19 +0100] rev 1347
merge
2010-03-05 Lift fv and bn eqvts; no need to lift alpha_eqvt.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 14:55:21 +0100] rev 1346
Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Not much progress about the single existential let case.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 13:04:47 +0100] rev 1345
Not much progress about the single existential let case.
2010-03-05 Fixed LF for one quantifier over 2 premises.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 10:23:40 +0100] rev 1344
Fixed LF for one quantifier over 2 premises.
2010-03-05 Trying to fix the proofs for the single existential... So far failed.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 05 Mar 2010 09:41:22 +0100] rev 1343
Trying to fix the proofs for the single existential... So far failed.
2010-03-04 Lift distinct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 18:57:23 +0100] rev 1342
Lift distinct.
2010-03-04 Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:55:53 +0100] rev 1341
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 15:15:44 +0100] rev 1340
Lift BV,FV,Permutations and injection :).
2010-03-04 Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 12:00:11 +0100] rev 1339
Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04 A version that just leaves the supp/\supp goal. Obviously not true.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 11:16:36 +0100] rev 1338
A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Prove symp and transp of weird without the supp /\ supp = {} assumption.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 04 Mar 2010 10:59:52 +0100] rev 1337
Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:51:47 +0100] rev 1336
merge
2010-03-03 Experiments with proving weird transp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:49:34 +0100] rev 1335
Experiments with proving weird transp
2010-03-03 Code for solving symp goals with multiple existentials.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 17:47:29 +0100] rev 1334
Code for solving symp goals with multiple existentials.
2010-03-03 reflp for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 15:28:25 +0100] rev 1333
reflp for multiple quantifiers.
2010-03-03 fixed mess in Test.thy
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 14:46:14 +0100] rev 1332
fixed mess in Test.thy
2010-03-03 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 14:22:58 +0100] rev 1331
Fix eqvt for multiple quantifiers.
2010-03-03 only tuned
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:48:05 +0100] rev 1330
only tuned
2010-03-03 merged
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:47:06 +0100] rev 1329
merged
2010-03-03 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 12:45:55 +0100] rev 1328
start of paper - does not compile yet
2010-03-03 added ACM style file for ICFP
Christian Urban <urbanc@in.tum.de> [Wed, 03 Mar 2010 11:50:25 +0100] rev 1327
added ACM style file for ICFP
2010-03-03 weird eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 11:42:15 +0100] rev 1326
weird eqvt
2010-03-03 Add the supp intersection conditions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 03 Mar 2010 10:39:43 +0100] rev 1325
Add the supp intersection conditions.
2010-03-02 Comment out the part that does not work with 2 quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 21:43:27 +0100] rev 1324
Comment out the part that does not work with 2 quantifiers.
2010-03-02 Fixes for the fv problem and alpha problem.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 21:10:04 +0100] rev 1323
Fixes for the fv problem and alpha problem.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 20:14:21 +0100] rev 1322
merged
2010-03-02 preliinary test about alpha-weirdo
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 20:11:56 +0100] rev 1321
preliinary test about alpha-weirdo
2010-03-02 Another problem with permutations in alpha and possibly also in fv
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 18:57:26 +0100] rev 1320
Another problem with permutations in alpha and possibly also in fv
2010-03-02 potential problem with the phd-example, where two permutations are generated, but only one is used
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 18:48:20 +0100] rev 1319
potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Some tests around Term4. Not sure how to fix the generated fv function.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 19:48:44 +0100] rev 1318
Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:48:56 +0100] rev 1317
merge
2010-03-02 Porting from Lift to Parser; until defining the Quotient type.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:48:41 +0100] rev 1316
Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Add image_eqvt and atom_eqvt to eqvt bases.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:11:58 +0100] rev 1315
Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Include the raw eqvt lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 17:11:19 +0100] rev 1314
Include the raw eqvt lemmas.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 16:04:48 +0100] rev 1313
merged
2010-03-02 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 16:03:19 +0100] rev 1312
added some more examples from Peter Sewell's bestiary
2010-03-02 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:13:00 +0100] rev 1311
merge
2010-03-02 Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:12:50 +0100] rev 1310
Minor
2010-03-02 Working bv_eqvt
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:11:41 +0100] rev 1309
Working bv_eqvt
2010-03-02 Moving wrappers out of Lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 15:10:47 +0100] rev 1308
Moving wrappers out of Lift.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 15:07:27 +0100] rev 1307
merged
2010-03-02 added distinctness of perms
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 15:05:50 +0100] rev 1306
added distinctness of perms
2010-03-02 updated (added lemma about commuting permutations)
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 15:05:35 +0100] rev 1305
updated (added lemma about commuting permutations)
2010-03-02 Change type schemes to name set.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 14:51:40 +0100] rev 1304
Change type schemes to name set.
2010-03-02 More fixes for new alpha, the whole lift script should now work again.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 14:24:57 +0100] rev 1303
More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Length fix for nested recursions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 13:28:54 +0100] rev 1302
Length fix for nested recursions.
2010-03-02 Fix equivp.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 12:28:07 +0100] rev 1301
Fix equivp.
2010-03-02 Fixed eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 11:04:49 +0100] rev 1300
Fixed eqvt code.
2010-03-02 most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 08:58:28 +0100] rev 1299
most tests work - the ones that do not I commented out
2010-03-02 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 08:49:04 +0100] rev 1298
merge
2010-03-02 Add a check of fv_functions.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 08:48:35 +0100] rev 1297
Add a check of fv_functions.
2010-03-02 some tuning
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 08:43:53 +0100] rev 1296
some tuning
2010-03-02 Link calls to Raw permutations, FV definition and alpha_definition into the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 02 Mar 2010 08:42:10 +0100] rev 1295
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 merged
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 06:43:09 +0100] rev 1294
merged
2010-03-02 rawified the bind specs (ready to be used now)
Christian Urban <urbanc@in.tum.de> [Tue, 02 Mar 2010 06:42:43 +0100] rev 1293
rawified the bind specs (ready to be used now)
2010-03-01 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Mar 2010 21:50:40 +0100] rev 1292
merge
2010-03-01 Trying to prove equivariance.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Mar 2010 21:50:24 +0100] rev 1291
Trying to prove equivariance.
2010-03-01 modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de> [Mon, 01 Mar 2010 19:23:08 +0100] rev 1290
modified for new binding format - hope it is the intended one
2010-03-01 further code-refactoring in the parser
Christian Urban <urbanc@in.tum.de> [Mon, 01 Mar 2010 16:55:41 +0100] rev 1289
further code-refactoring in the parser
2010-03-01 The new alpha-equivalence and testing in Trm2 and Trm5.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Mar 2010 16:04:03 +0100] rev 1288
The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01 slight simplification of the raw-decl generation
Christian Urban <urbanc@in.tum.de> [Mon, 01 Mar 2010 14:26:14 +0100] rev 1287
slight simplification of the raw-decl generation
2010-03-01 Example that shows that current alpha is wrong.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 01 Mar 2010 11:40:48 +0100] rev 1286
Example that shows that current alpha is wrong.
2010-03-01 added example from my phd
Christian Urban <urbanc@in.tum.de> [Mon, 01 Mar 2010 07:46:50 +0100] rev 1285
added example from my phd
2010-02-27 streamlined parser
Christian Urban <urbanc@in.tum.de> [Sat, 27 Feb 2010 11:54:59 +0100] rev 1284
streamlined parser
2010-02-26 generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
Christian Urban <urbanc@in.tum.de> [Fri, 26 Feb 2010 18:38:25 +0100] rev 1283
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26 More about the general lifting procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 18:21:39 +0100] rev 1282
More about the general lifting procedure.
2010-02-26 Update TODO
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 16:22:47 +0100] rev 1281
Update TODO
2010-02-26 Progress with general lifting procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 16:15:03 +0100] rev 1280
Progress with general lifting procedure.
2010-02-26 RSP of perms can be shown in one go.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 15:42:00 +0100] rev 1279
RSP of perms can be shown in one go.
2010-02-26 Change in signature of prove_const_rsp for general lifting.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 15:10:55 +0100] rev 1278
Change in signature of prove_const_rsp for general lifting.
2010-02-26 Permutation and FV_Alpha interface change.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 13:57:43 +0100] rev 1277
Permutation and FV_Alpha interface change.
2010-02-26 To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 26 Feb 2010 10:34:04 +0100] rev 1276
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-25 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 15:41:23 +0100] rev 1275
merge
2010-02-25 Preparing the generalized lifting procedure
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 15:40:09 +0100] rev 1274
Preparing the generalized lifting procedure
2010-02-25 merged
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 14:20:40 +0100] rev 1273
merged
2010-02-25 added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 14:20:10 +0100] rev 1272
added ott-example about Leroy96
2010-02-25 Forgot to add one file.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 14:14:40 +0100] rev 1271
Forgot to add one file.
2010-02-25 Split Terms into separate files and add them to tests.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 14:14:08 +0100] rev 1270
Split Terms into separate files and add them to tests.
2010-02-25 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 12:32:15 +0100] rev 1269
merge
2010-02-25 Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 12:30:50 +0100] rev 1268
Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25 merged
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 12:24:37 +0100] rev 1267
merged
2010-02-25 a few simplifications
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 11:51:34 +0100] rev 1266
a few simplifications
2010-02-25 first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 11:30:00 +0100] rev 1265
first attempt to make sense out of the core-haskell definition
2010-02-25 Code for proving eqvt, still in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 12:15:11 +0100] rev 1264
Code for proving eqvt, still in Terms.
2010-02-25 Use eqvt infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 09:41:14 +0100] rev 1263
Use eqvt infrastructure.
2010-02-25 Simple function eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 09:22:29 +0100] rev 1262
Simple function eqvt code.
2010-02-25 added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 08:40:52 +0100] rev 1261
added IsaMakefile...but so far included only a test for the parser
2010-02-25 moved Quot package to Attic (still compiles there with "isabelle make")
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 07:57:17 +0100] rev 1260
moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25 merged
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 07:48:57 +0100] rev 1259
merged
2010-02-25 moved Nominal to "toplevel"
Christian Urban <urbanc@in.tum.de> [Thu, 25 Feb 2010 07:48:33 +0100] rev 1258
moved Nominal to "toplevel"
2010-02-25 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 25 Feb 2010 07:05:52 +0100] rev 1257
Export perm_frees.
2010-02-24 Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 23:25:30 +0100] rev 1256
Restructuring the code in Perm
2010-02-24 Simplified and finised eqvt proofs for t1 and t5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 18:38:49 +0100] rev 1255
Simplified and finised eqvt proofs for t1 and t5
2010-02-24 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 17:42:52 +0100] rev 1254
merge
2010-02-24 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 17:42:37 +0100] rev 1253
Define lifted perms.
2010-02-24 merged
Christian Urban <urbanc@in.tum.de> [Wed, 24 Feb 2010 17:32:43 +0100] rev 1252
merged
2010-02-24 parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de> [Wed, 24 Feb 2010 17:32:22 +0100] rev 1251
parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24 With permute_rsp we can lift the instance proofs :).
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 15:39:17 +0100] rev 1250
With permute_rsp we can lift the instance proofs :).
2010-02-24 Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 15:36:07 +0100] rev 1249
Note the instance proofs, since they can be easily lifted.
2010-02-24 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 15:13:22 +0100] rev 1248
More refactoring and removed references to the global simpset in Perm.
2010-02-24 Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 14:55:09 +0100] rev 1247
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24 Regularize finite support proof for trm1
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 14:37:51 +0100] rev 1246
Regularize finite support proof for trm1
2010-02-24 Made the fv-supp proof much more straightforward.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 14:09:34 +0100] rev 1245
Made the fv-supp proof much more straightforward.
2010-02-24 Regularize the proofs about finite support.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 12:06:55 +0100] rev 1244
Regularize the proofs about finite support.
2010-02-24 Respects of permute and constructors.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 11:28:34 +0100] rev 1243
Respects of permute and constructors.
2010-02-24 Generate fv_rsp automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 11:03:30 +0100] rev 1242
Generate fv_rsp automatically.
2010-02-24 Define the constants automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:59:31 +0100] rev 1241
Define the constants automatically.
2010-02-24 Rename also the lifted types to non-capital.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:47:41 +0100] rev 1240
Rename also the lifted types to non-capital.
2010-02-24 Use the infrastructure in LF. Much shorter :).
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:44:38 +0100] rev 1239
Use the infrastructure in LF. Much shorter :).
2010-02-24 Final synchronization of names.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:38:45 +0100] rev 1238
Final synchronization of names.
2010-02-24 LF renaming part 3 (proper names of alpha equvalences)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:25:59 +0100] rev 1237
LF renaming part 3 (proper names of alpha equvalences)
2010-02-24 LF renaming part 2 (proper fv functions)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 10:08:54 +0100] rev 1236
LF renaming part 2 (proper fv functions)
2010-02-24 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 09:58:44 +0100] rev 1235
merge
2010-02-24 LF renaming part1.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 24 Feb 2010 09:58:12 +0100] rev 1234
LF renaming part1.
2010-02-24 merged
Christian Urban <urbanc@in.tum.de> [Wed, 24 Feb 2010 09:56:32 +0100] rev 1233
merged
2010-02-24 parsing of function definitions almost works now; still an error with undefined constants
Christian Urban <urbanc@in.tum.de> [Wed, 24 Feb 2010 09:56:12 +0100] rev 1232
parsing of function definitions almost works now; still an error with undefined constants
2010-02-23 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 18:28:48 +0100] rev 1231
merge
2010-02-23 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 18:27:32 +0100] rev 1230
rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23 merged
Christian Urban <urbanc@in.tum.de> [Tue, 23 Feb 2010 16:32:04 +0100] rev 1229
merged
2010-02-23 declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de> [Tue, 23 Feb 2010 16:31:40 +0100] rev 1228
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
2010-02-23 rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 16:12:30 +0100] rev 1227
rsp infrastructure.
2010-02-23 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 14:20:42 +0100] rev 1226
merge
2010-02-23 Progress towards automatic rsp of constants and fv.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 14:19:44 +0100] rev 1225
Progress towards automatic rsp of constants and fv.
2010-02-23 merged
Christian Urban <urbanc@in.tum.de> [Tue, 23 Feb 2010 13:33:01 +0100] rev 1224
merged
2010-02-23 "raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de> [Tue, 23 Feb 2010 13:32:35 +0100] rev 1223
"raw"-ified the term-constructors and types given in the specification
2010-02-23 Looking at proving the rsp rules automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 12:49:45 +0100] rev 1222
Looking at proving the rsp rules automatically.
2010-02-23 Minor beutification.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 11:56:47 +0100] rev 1221
Minor beutification.
2010-02-23 Define the quotient from ML
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 11:22:06 +0100] rev 1220
Define the quotient from ML
2010-02-23 All works in LF but will require renaming.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 10:47:14 +0100] rev 1219
All works in LF but will require renaming.
2010-02-23 Reordering in LF.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 09:34:41 +0100] rev 1218
Reordering in LF.
2010-02-23 Fixes for auxiliary datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 23 Feb 2010 09:31:59 +0100] rev 1217
Fixes for auxiliary datatypes.
2010-02-22 Fixed pseudo_injectivity for trm4
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 18:09:44 +0100] rev 1216
Fixed pseudo_injectivity for trm4
2010-02-22 Testing auto equivp code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 17:19:28 +0100] rev 1215
Testing auto equivp code.
2010-02-22 A tactic for final equivp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 16:44:58 +0100] rev 1214
A tactic for final equivp
2010-02-22 More equivp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 16:16:04 +0100] rev 1213
More equivp infrastructure.
2010-02-22 tactify transp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 15:41:30 +0100] rev 1212
tactify transp
2010-02-22 export the reflp and symp tacs.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 15:09:53 +0100] rev 1211
export the reflp and symp tacs.
2010-02-22 Generalize atom_trans and atom_sym.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 15:03:48 +0100] rev 1210
Generalize atom_trans and atom_sym.
2010-02-22 Some progress about transp
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 14:50:53 +0100] rev 1209
Some progress about transp
2010-02-22 alpha-symmetric addons.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 13:41:13 +0100] rev 1208
alpha-symmetric addons.
2010-02-22 alpha reflexivity
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 12:12:32 +0100] rev 1207
alpha reflexivity
2010-02-22 Renaming.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 10:57:39 +0100] rev 1206
Renaming.
2010-02-22 Added missing description.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 10:39:05 +0100] rev 1205
Added missing description.
2010-02-22 Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 10:16:13 +0100] rev 1204
Added Brian's suggestion.
2010-02-22 Update TODO
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 22 Feb 2010 09:55:43 +0100] rev 1203
Update TODO
2010-02-21 Removed bindings 'in itself' where possible.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sun, 21 Feb 2010 22:39:11 +0100] rev 1202
Removed bindings 'in itself' where possible.
2010-02-20 Some adaptation
Cezary Kaliszyk <kaliszyk@in.tum.de> [Sat, 20 Feb 2010 06:31:03 +0100] rev 1201
Some adaptation
2010-02-19 proof cleaning and standardizing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Feb 2010 17:50:43 +0100] rev 1200
proof cleaning and standardizing.
2010-02-19 Automatic production and proving of pseudo-injectivity.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Feb 2010 16:45:24 +0100] rev 1199
Automatic production and proving of pseudo-injectivity.
2010-02-19 Experiments for the pseudo-injectivity tactic.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Feb 2010 12:05:58 +0100] rev 1198
Experiments for the pseudo-injectivity tactic.
2010-02-19 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Feb 2010 10:26:38 +0100] rev 1197
merge
2010-02-19 Constructing alpha_inj goal.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Feb 2010 10:17:35 +0100] rev 1196
Constructing alpha_inj goal.
2010-02-18 merged
Christian Urban <urbanc@in.tum.de> [Thu, 18 Feb 2010 23:07:52 +0100] rev 1195
merged
2010-02-18 start work with the parser
Christian Urban <urbanc@in.tum.de> [Thu, 18 Feb 2010 23:07:28 +0100] rev 1194
start work with the parser
2010-02-18 Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 18:33:53 +0100] rev 1193
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18 First (non-working) version of alpha-equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 15:03:09 +0100] rev 1192
First (non-working) version of alpha-equivalence
2010-02-18 Description of the fv procedure.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 13:36:38 +0100] rev 1191
Description of the fv procedure.
2010-02-18 Testing auto constant lifting.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 12:06:59 +0100] rev 1190
Testing auto constant lifting.
2010-02-18 Fix for new Isabelle (primrec)
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 11:28:20 +0100] rev 1189
Fix for new Isabelle (primrec)
2010-02-18 Automatic lifting of constants.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 11:19:16 +0100] rev 1188
Automatic lifting of constants.
2010-02-18 Changed back to original version of trm5
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 10:01:48 +0100] rev 1187
Changed back to original version of trm5
2010-02-18 The alternate version of trm5 with additional binding. All proofs work the same.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 10:00:58 +0100] rev 1186
The alternate version of trm5 with additional binding. All proofs work the same.
2010-02-18 Code for handling atom sets.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 09:46:38 +0100] rev 1185
Code for handling atom sets.
2010-02-18 Replace Terms by Terms2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 08:43:13 +0100] rev 1184
Replace Terms by Terms2.
2010-02-18 Fixed proofs in Terms2 and found a mistake in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 18 Feb 2010 08:37:45 +0100] rev 1183
Fixed proofs in Terms2 and found a mistake in Terms.
2010-02-17 Terms2 with bindings for binders synchronized with bindings they are used in.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 17:51:35 +0100] rev 1182
Terms2 with bindings for binders synchronized with bindings they are used in.
2010-02-17 Cleaning of proofs in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 17:29:26 +0100] rev 1181
Cleaning of proofs in Terms.
2010-02-17 Testing Fv
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 16:22:16 +0100] rev 1180
Testing Fv
2010-02-17 Fix the strong induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 15:52:08 +0100] rev 1179
Fix the strong induction principle.
2010-02-17 Reorder
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 15:45:03 +0100] rev 1178
Reorder
2010-02-17 Add bindings of recursive types by free_variables.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 15:28:50 +0100] rev 1177
Add bindings of recursive types by free_variables.
2010-02-17 Bindings adapted to multiple defined datatypes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 15:20:22 +0100] rev 1176
Bindings adapted to multiple defined datatypes.
2010-02-17 Reorganization
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 15:00:04 +0100] rev 1175
Reorganization
2010-02-17 Now should work.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 14:44:32 +0100] rev 1174
Now should work.
2010-02-17 Some optimizations and fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 14:35:06 +0100] rev 1173
Some optimizations and fixes.
2010-02-17 Simplified format of bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 14:17:02 +0100] rev 1172
Simplified format of bindings.
2010-02-17 Tested the Perm code; works everywhere in Terms.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 13:56:31 +0100] rev 1171
Tested the Perm code; works everywhere in Terms.
2010-02-17 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 13:54:35 +0100] rev 1170
Wrapped the permutation code.
2010-02-17 Description of intended bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 10:20:26 +0100] rev 1169
Description of intended bindings.
2010-02-17 Code for generating the fv function, no bindings yet.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 10:12:01 +0100] rev 1168
Code for generating the fv function, no bindings yet.
2010-02-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 09:27:02 +0100] rev 1167
merge
2010-02-17 indent
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 09:26:49 +0100] rev 1166
indent
2010-02-17 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 09:26:38 +0100] rev 1165
merge
2010-02-17 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 17 Feb 2010 09:26:10 +0100] rev 1164
Simplifying perm_eq
2010-02-16 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Feb 2010 15:13:14 +0100] rev 1163
merge
2010-02-16 indenting
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Feb 2010 15:12:31 +0100] rev 1162
indenting
2010-02-16 Minor
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Feb 2010 15:12:49 +0100] rev 1161
Minor
2010-02-16 Merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Feb 2010 14:57:39 +0100] rev 1160
Merge
2010-02-16 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Tue, 16 Feb 2010 14:57:22 +0100] rev 1159
Ported Stefan's permutation code, still needs some localizing.
2010-02-15 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:54:09 +0100] rev 1158
merge
2010-02-15 Removed varifyT.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:53:51 +0100] rev 1157
Removed varifyT.
2010-02-15 merged
Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 17:02:46 +0100] rev 1156
merged
2010-02-15 2-spaces rule (where it makes sense)
Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 17:02:26 +0100] rev 1155
2-spaces rule (where it makes sense)
2010-02-15 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:52:32 +0100] rev 1154
merge
2010-02-15 Fixed the definition of less and finished the missing proof.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 16:51:30 +0100] rev 1153
Fixed the definition of less and finished the missing proof.
2010-02-15 further tuning
Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:50:11 +0100] rev 1152
further tuning
2010-02-15 small tuning
Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:37:48 +0100] rev 1151
small tuning
2010-02-15 tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
Christian Urban <urbanc@in.tum.de> [Mon, 15 Feb 2010 16:28:07 +0100] rev 1150
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
2010-02-15 der_bname -> derived_bname
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:58:03 +0100] rev 1149
der_bname -> derived_bname
2010-02-15 Names of files.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:51:17 +0100] rev 1148
Names of files.
2010-02-15 Finished introducing the binding.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 14:28:03 +0100] rev 1147
Finished introducing the binding.
2010-02-15 Synchronize the commands.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 13:40:03 +0100] rev 1146
Synchronize the commands.
2010-02-15 Passing the binding to quotient_def
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 12:23:02 +0100] rev 1145
Passing the binding to quotient_def
2010-02-15 Added a binding to the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 12:15:14 +0100] rev 1144
Added a binding to the parser.
2010-02-15 Second inline
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 10:25:17 +0100] rev 1143
Second inline
2010-02-15 remove one-line wrapper.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Mon, 15 Feb 2010 10:11:26 +0100] rev 1142
remove one-line wrapper.
2010-02-12 Undid the read_terms change; now compiles.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Feb 2010 16:27:25 +0100] rev 1141
Undid the read_terms change; now compiles.
2010-02-12 merge
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Feb 2010 16:06:09 +0100] rev 1140
merge
2010-02-12 renamed 'as' to 'is' everywhere.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Feb 2010 16:04:10 +0100] rev 1139
renamed 'as' to 'is' everywhere.
2010-02-12 "is" defined as the keyword
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Feb 2010 15:50:43 +0100] rev 1138
"is" defined as the keyword
2010-02-12 moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de> [Fri, 12 Feb 2010 15:06:20 +0100] rev 1137
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
2010-02-12 The lattice instantiations are gone from Isabelle/Main, so
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 12 Feb 2010 12:06:09 +0100] rev 1136
The lattice instantiations are gone from Isabelle/Main, so this can be removed.
2010-02-11 the lam/bla example.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 17:58:06 +0100] rev 1135
the lam/bla example.
2010-02-11 Finished a working foo/bar.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 16:54:04 +0100] rev 1134
Finished a working foo/bar.
2010-02-11 fv_foo is not regular.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 16:05:15 +0100] rev 1133
fv_foo is not regular.
2010-02-11 Testing foo/bar
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 15:08:45 +0100] rev 1132
Testing foo/bar
2010-02-11 Even when bv = fv it still doesn't lift.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 14:23:26 +0100] rev 1131
Even when bv = fv it still doesn't lift.
2010-02-11 Added the missing syntax file
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 14:02:34 +0100] rev 1130
Added the missing syntax file
2010-02-11 Notation available locally
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 14:00:00 +0100] rev 1129
Notation available locally
2010-02-11 Main renaming + fixes for new Isabelle in IntEx2.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 10:06:02 +0100] rev 1128
Main renaming + fixes for new Isabelle in IntEx2.
2010-02-11 Merging QuotBase into QuotMain.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Thu, 11 Feb 2010 09:23:59 +0100] rev 1127
Merging QuotBase into QuotMain.
2010-02-10 removed dead code
Christian Urban <urbanc@in.tum.de> [Wed, 10 Feb 2010 21:39:40 +0100] rev 1126
removed dead code
2010-02-10 cleaned a bit
Christian Urban <urbanc@in.tum.de> [Wed, 10 Feb 2010 20:35:54 +0100] rev 1125
cleaned a bit
2010-02-10 lowercase locale
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 17:22:18 +0100] rev 1124
lowercase locale
2010-02-10 hg-added the added file.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 17:10:52 +0100] rev 1123
hg-added the added file.
2010-02-10 Changes from Makarius's code review + some noticed fixes.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 17:02:29 +0100] rev 1122
Changes from Makarius's code review + some noticed fixes.
2010-02-10 example with a respectful bn function defined over the type itself
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 12:30:26 +0100] rev 1121
example with a respectful bn function defined over the type itself
2010-02-10 Finishe the renaming.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 11:53:15 +0100] rev 1120
Finishe the renaming.
2010-02-10 Another mistake found with OTT.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Wed, 10 Feb 2010 11:39:22 +0100] rev 1119
Another mistake found with OTT.
(0) -1000 -240 +240 +1000 tip