| Thu, 12 Feb 2015 12:46:50 +0000 |
paulson |
new lemmas re refinement of one equivalence relation WRT another
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 21:22:01 +0100 |
blanchet |
hide short const name
|
file |
diff |
annotate
|
| Thu, 16 Jan 2014 18:52:50 +0100 |
blanchet |
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 19:34:52 +0100 |
haftmann |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
dropped references to obsolete fact `mem_def`
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 14:01:06 +0200 |
haftmann |
avoid duplicated simp add option
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 07:17:15 +0900 |
Cezary Kaliszyk |
Quotient Package: make quotient_type work with separate set type
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 20:38:58 +0100 |
wenzelm |
recoded latin1 as utf8;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 22:41:17 +0100 |
haftmann |
replaced slightly odd locale congruent2 by plain definition
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 22:32:06 +0100 |
haftmann |
replaced slightly odd locale congruent by plain definition
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 13:44:54 +0100 |
haftmann |
equivI has replaced equiv.intro
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 12:14:43 +0100 |
haftmann |
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:03:42 +0100 |
haftmann |
Plain, Main form meeting points in import hierarchy
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:26 +0200 |
haftmann |
dropped superfluous code lemmas
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:33 +0200 |
berghofe |
Instantiated subst rule to avoid problems with HO unification.
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:37 +0100 |
haftmann |
dropped implicit assumption proof
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:43 +0200 |
haftmann |
moved finite lemmas to Finite_Set.thy
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:49 +0100 |
wenzelm |
respects2: tuned spacing;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 03 Jul 2006 20:02:42 +0200 |
nipkow |
replaced translation by abbreviation
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 20:03:53 +0100 |
nipkow |
Converted translations to abbbreviations.
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 17:57:09 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 13:00:53 +0100 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
| Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 18:30:59 +0100 |
nipkow |
First step in reorganizing Finite_Set
|
file |
diff |
annotate
|
| Sun, 21 Nov 2004 15:44:20 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sun, 21 Nov 2004 12:52:03 +0100 |
nipkow |
Restructured List and added "rotate"
|
file |
diff |
annotate
|
| Fri, 19 Nov 2004 17:31:49 +0100 |
paulson |
moved and renamed Integ/Equiv.thy
|
file |
diff |
annotate
|