| Thu, 05 Apr 2012 15:59:25 +0200 |
huffman |
add transfer lemmas for quotients
|
changeset |
files
|
| 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
|
| Wed, 04 Apr 2012 17:51:12 +0200 |
kuncar |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
changeset |
files
|
| Wed, 04 Apr 2012 16:29:17 +0100 |
sultana |
tuned;
|
changeset |
files
|
| Wed, 04 Apr 2012 16:29:16 +0100 |
sultana |
added interpretation for formula conditional;
|
changeset |
files
|
| Wed, 04 Apr 2012 16:29:16 +0100 |
sultana |
refactored tptp lex;
|
changeset |
files
|
| Wed, 04 Apr 2012 16:29:16 +0100 |
sultana |
refactored tptp yacc to bring close to official spec;
|
changeset |
files
|
| Wed, 04 Apr 2012 16:05:52 +0200 |
huffman |
transfer method generalizes over free variables in goal
|
changeset |
files
|
| Wed, 04 Apr 2012 16:03:01 +0200 |
huffman |
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
|
changeset |
files
|
| Wed, 04 Apr 2012 12:25:58 +0200 |
huffman |
update keywords file
|
changeset |
files
|
| Wed, 04 Apr 2012 14:27:20 +0200 |
huffman |
merged
|
changeset |
files
|
| Wed, 04 Apr 2012 11:50:08 +0200 |
huffman |
fix typos
|
changeset |
files
|
| Wed, 04 Apr 2012 13:42:01 +0200 |
huffman |
lift_definition command generates transfer rule
|
changeset |
files
|
| Wed, 04 Apr 2012 13:41:38 +0200 |
huffman |
prove_quot_theorem fixes types
|
changeset |
files
|
| Wed, 04 Apr 2012 14:08:24 +0200 |
bulwahn |
documenting options quickcheck_locale; adjusting IsarRef documentation of Quotient predicate; NEWS
|
changeset |
files
|
| Wed, 04 Apr 2012 12:22:51 +0200 |
bulwahn |
added option quickcheck_locale to allow different behaviours for handling locales in Quickcheck;
|
changeset |
files
|
| Fri, 06 Apr 2012 12:02:24 +0200 |
wenzelm |
stop node execution at first unassigned exec;
|
changeset |
files
|