| Tue, 04 May 2010 08:55:43 +0200 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
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
|
| Thu, 11 Mar 2010 14:40:29 +0100 |
haftmann |
Big_Operators now in Main rather than Plain
|
file |
diff |
annotate
|
| Wed, 10 Mar 2010 16:53:27 +0100 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:27:16 +0100 |
krauss |
authentic constants; moved "acyclic" further down
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:57 +0100 |
krauss |
point-free characterization of well-foundedness
|
file |
diff |
annotate
|
| Mon, 26 Oct 2009 23:26:18 +0100 |
krauss |
replaced (outdated) comments by explicit statements
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:32:53 +0200 |
haftmann |
simplified proof
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:48 +0200 |
krauss |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:34:44 +0200 |
krauss |
moved wfrec to Recdef.thy
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 20:32:00 +0200 |
krauss |
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 13:37:08 +0200 |
haftmann |
explicit is better than implicit
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 08:48:56 +0200 |
krauss |
moved obsolete same_fst to Recdef.thy
|
file |
diff |
annotate
|