| 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: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
|
| Wed, 16 May 2012 19:15:45 +0200 |
kuncar |
infrastructure that makes possible to prove that a relation is reflexive
|
file |
diff |
annotate
|
| Fri, 04 May 2012 17:12:37 +0200 |
huffman |
lifting package produces abs_eq_iff rules for total quotients
|
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
|
| Mon, 23 Apr 2012 17:18:18 +0200 |
kuncar |
move MRSL to a separate file
|
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 13:06:22 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 19 Apr 2012 08:45:13 +0200 |
huffman |
generate abs_induct rules for quotient types
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 17:04:03 +0200 |
kuncar |
Lifting: generate more thms & note them & tuned
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 15:48:32 +0200 |
huffman |
move constant 'Respects' into Lifting.thy;
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 15:09:07 +0200 |
huffman |
add lemma Quotient_abs_induct
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:59:04 +0200 |
huffman |
more usage of context blocks
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 14:34:25 +0200 |
huffman |
use context block
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 12:15:20 +0200 |
huffman |
lifting_setup generates transfer rule for rep of typedefs
|
file |
diff |
annotate
|
| Wed, 18 Apr 2012 10:52:49 +0200 |
huffman |
use context block to organize typedef lifting theorems
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 19:16:13 +0200 |
kuncar |
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
|
file |
diff |
annotate
|
| Mon, 16 Apr 2012 20:50:43 +0200 |
kuncar |
leave Lifting prefix
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 11:01:15 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 15:15:48 +0900 |
griff |
manual merge
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 15:59:25 +0200 |
huffman |
add transfer lemmas for quotients
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 20:45:19 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 16:48:39 +0200 |
huffman |
add lemmas for generating transfer rules for typedefs
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 17:51:12 +0200 |
kuncar |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 12:25:58 +0200 |
huffman |
update keywords file
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 13:42:01 +0200 |
huffman |
lift_definition command generates transfer rule
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 22:31:00 +0200 |
huffman |
new transfer proof method
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|