| Thu, 05 Apr 2012 15:23:26 +0200 |
huffman |
define reflp directly, in the manner of symp and transp
|
changeset |
files
|
| Thu, 05 Apr 2012 14:14:16 +0200 |
huffman |
set up and use lift_definition for word operations
|
changeset |
files
|
| Thu, 05 Apr 2012 12:18:06 +0200 |
huffman |
lift_definition declares transfer_rule attribute
|
changeset |
files
|
| Thu, 05 Apr 2012 10:48:46 +0200 |
huffman |
configure transfer method for 'a word -> int
|
changeset |
files
|
| Thu, 05 Apr 2012 08:43:31 +0200 |
krauss |
added timestamps to logging of named thms
|
changeset |
files
|
| Thu, 05 Apr 2012 08:13:40 +0200 |
huffman |
merged
|
changeset |
files
|
| Wed, 04 Apr 2012 20:45:19 +0200 |
huffman |
merged
|
changeset |
files
|
| Wed, 04 Apr 2012 16:48:39 +0200 |
huffman |
add lemmas for generating transfer rules for typedefs
|
changeset |
files
|
| Thu, 05 Apr 2012 00:37:22 +0100 |
sultana |
tuned;
|
changeset |
files
|
| Wed, 04 Apr 2012 21:57:39 +0100 |
sultana |
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;
|
changeset |
files
|
| Wed, 04 Apr 2012 20:40:39 +0200 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
| Wed, 04 Apr 2012 20:10:21 +0200 |
Cezary Kaliszyk |
HOL/Import more precise map types
|
changeset |
files
|
| Wed, 04 Apr 2012 20:09:56 +0200 |
Cezary Kaliszyk |
HOL/Import typed matches against Isabelle typedef result
|
changeset |
files
|
| Wed, 04 Apr 2012 19:20:52 +0200 |
kuncar |
connect the Quotient package to the Lifting package
|
changeset |
files
|