| Wed, 18 Apr 2012 15:09:07 +0200 | huffman | add lemma Quotient_abs_induct | changeset | files |
| Wed, 18 Apr 2012 14:59:04 +0200 | huffman | more usage of context blocks | changeset | files |
| Wed, 18 Apr 2012 14:34:25 +0200 | huffman | use context block | changeset | files |
| Wed, 18 Apr 2012 12:15:20 +0200 | huffman | lifting_setup generates transfer rule for rep of typedefs | changeset | files |
| Wed, 18 Apr 2012 10:52:49 +0200 | huffman | use context block to organize typedef lifting theorems | changeset | files |
| Wed, 18 Apr 2012 10:53:28 +0200 | blanchet | avoid generating syntactically invalid patterns (with "if_then_else") in SMT-LIB files | changeset | files |
| Wed, 18 Apr 2012 10:53:28 +0200 | blanchet | compile | changeset | files |