| Mon, 20 Jan 2014 20:42:43 +0100 |
blanchet |
rationalized lemmas
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
new parametricity rules and useful lemmas
|
file |
diff |
annotate
|
| Fri, 27 Sep 2013 09:07:45 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 15:50:33 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
|
file |
diff |
annotate
|
| Mon, 10 Jun 2013 06:08:12 -0700 |
huffman |
implement 'untransferred' attribute, which is like 'transferred' but works in the opposite direction
|
file |
diff |
annotate
|
| Sat, 08 Jun 2013 19:40:19 -0700 |
huffman |
implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
|
file |
diff |
annotate
|
| Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
file |
diff |
annotate
|
| Mon, 13 May 2013 12:13:24 +0200 |
kuncar |
try to detect assumptions of transfer rules that are in a shape of a transfer rule
|
file |
diff |
annotate
|
| Sat, 16 Mar 2013 20:51:23 +0100 |
kuncar |
fixing transfer tactic - unfold fully identity relation by using relator_eq
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: more flexible handling of equality relations using is_equality predicate
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Wed, 16 May 2012 19:17:20 +0200 |
kuncar |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
file |
diff |
annotate
|
| Tue, 15 May 2012 11:50:34 +0200 |
huffman |
add transfer rules for nat_rec and funpow
|
file |
diff |
annotate
|
| Fri, 27 Apr 2012 14:07:31 +0200 |
huffman |
implement transfer tactic with more scalable forward proof methods
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 21:32:35 +0200 |
huffman |
tuned precedence order of transfer rules
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 11:05:04 +0200 |
huffman |
new example theory for quotient/transfer
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 20:52:33 +0200 |
huffman |
enable variant of transfer method that proves an implication instead of an equivalence
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:05:07 +0200 |
huffman |
add transfer rule for nat_case
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:54:13 +0200 |
huffman |
uniform naming scheme for transfer rules
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 22:49:40 +0200 |
huffman |
rename 'correspondence' method to 'transfer_prover'
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 15:49:45 +0200 |
huffman |
add secondary transfer rule for universal quantifiers on non-bi-total relations
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 15:30:13 +0200 |
huffman |
add transfer rule for 'id'
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 10:18:08 +0200 |
huffman |
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 19:36:09 +0200 |
huffman |
add transfer rule for Let
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 14:00:09 +0200 |
huffman |
make transfer method more deterministic by using SOLVED' on some subgoals
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 11:03:08 +0200 |
huffman |
add theory data for relator identity rules;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:03:01 +0200 |
huffman |
add bounded quantifier constant transfer_bforall, whose definition is unfolded after transfer
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:31:00 +0200 |
huffman |
new transfer proof method
|
file |
diff |
annotate
|