| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
file |
diff |
annotate
|
| Mon, 10 Jun 2013 06:08:14 -0700 |
huffman |
more transfer rules for sets
|
file |
diff |
annotate
|
| Wed, 15 May 2013 12:10:39 +0200 |
kuncar |
stronger reflexivity prover
|
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
|
| Fri, 08 Mar 2013 13:21:52 +0100 |
kuncar |
add [relator_mono] and [relator_distr] rules
|
file |
diff |
annotate
|
| Thu, 24 May 2012 14:20:23 +0200 |
kuncar |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
file |
diff |
annotate
|
| Wed, 16 May 2012 19:15:45 +0200 |
kuncar |
infrastructure that makes possible to prove that a relation is reflexive
|
file |
diff |
annotate
|
| Mon, 14 May 2012 17:09:11 +0200 |
huffman |
add transfer rule for set_rel
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 12:01:58 +0200 |
kuncar |
use a quot_map theorem attribute instead of the complicated map attribute
|
file |
diff |
annotate
|
| Sun, 22 Apr 2012 20:16:30 +0200 |
huffman |
add transfer rule for set difference
|
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 13:12:27 +0200 |
huffman |
move alternative definition lemmas into Lifting.thy;
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 11:02:01 +0200 |
huffman |
added covariant relator set_rel, with transfer rules for set operations
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 10:59:52 +0200 |
huffman |
renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator
|
file |
diff |
annotate
|
| Fri, 20 Apr 2012 15:34:33 +0200 |
huffman |
move definition of set_rel into Library/Quotient_Set.thy
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 14:00:26 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:20:09 +0100 |
kuncar |
store the relational theorem for every relator
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 22:43:17 +0200 |
krauss |
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 10:59:22 +0900 |
Cezary Kaliszyk |
Quotient Package: add mem_rsp, mem_prs, tune proofs.
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 03:34:17 +0900 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
file |
diff |
annotate
|