| Sun, 01 Jan 2012 11:28:45 +0100 |
haftmann |
cleanup of code declarations
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:09 +0100 |
haftmann |
dropped obsolete code equation for Id
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 23:02:59 +0200 |
haftmann |
moved acyclic predicate up in hierarchy
|
file |
diff |
annotate
|
| Thu, 13 Oct 2011 22:56:19 +0200 |
haftmann |
modernized definitions
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 21:47:52 +0200 |
haftmann |
tuned specification and lemma distribution among theories; tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 13:33:28 +0100 |
bulwahn |
adding a definition for refl_on which is friendly for quickcheck and nitpick
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adding a nice definition of Id_on for quickcheck and nitpick
|
file |
diff |
annotate
|
| Sun, 09 May 2010 12:00:43 +0200 |
krauss |
added lemmas rel_comp_UNION_distrib(2)
|
file |
diff |
annotate
|
| Fri, 07 May 2010 15:03:57 +0200 |
krauss |
removed semicolons
|
file |
diff |
annotate
|
| Fri, 07 May 2010 15:03:53 +0200 |
krauss |
rule subrelI (for nice Isar proofs of relation inequalities)
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:27:24 +0100 |
krauss |
lemma converse_inv_image
|
file |
diff |
annotate
|