| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
daac7840 |
|
07-Aug-2017 |
blanchet <none@none> |
tuning imports
|
| #
9c6d59be |
|
10-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
81da5767 |
|
08-Jul-2015 |
haftmann <none@none> |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
| #
52933f0b |
|
18-Jun-2015 |
haftmann <none@none> |
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
--HG--
extra : rebase_source : 0045d1e39f330613bb1913e52e231f8be282a80a
|
| #
87979c1b |
|
11-Feb-2015 |
paulson <lp15@cam.ac.uk> |
new lemmas re refinement of one equivalence relation WRT another
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
1697504e |
|
16-Jan-2014 |
blanchet <none@none> |
hide short const name
|
| #
f339b90b |
|
16-Jan-2014 |
blanchet <none@none> |
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
|
| #
2c9578d4 |
|
15-Dec-2013 |
haftmann <none@none> |
more algebraic terminology for theories about big operators
|
| #
fa22b8b3 |
|
13-Feb-2013 |
haftmann <none@none> |
abandoned theory Plain
--HG--
extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5
|
| #
94314ed4 |
|
01-Mar-2012 |
haftmann <none@none> |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
| #
5aac7b14 |
|
24-Dec-2011 |
haftmann <none@none> |
dropped references to obsolete fact `mem_def`
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
c6ba3af4 |
|
18-Aug-2011 |
haftmann <none@none> |
avoid duplicated simp add option
|
| #
7994d347 |
|
18-Aug-2011 |
haftmann <none@none> |
observe distinction between sets and predicates more properly
|
| #
83a642c7 |
|
15-Aug-2011 |
Cezary Kaliszyk <kaliszyk@in.tum.de> |
Quotient Package: make quotient_type work with separate set type
|
| #
48096e82 |
|
03-Dec-2010 |
wenzelm <none@none> |
recoded latin1 as utf8;
use textcomp for some text symbols where it appears appropriate;
|
| #
c3d57e42 |
|
29-Nov-2010 |
haftmann <none@none> |
replaced slightly odd locale congruent2 by plain definition
|
| #
ba56a1d0 |
|
29-Nov-2010 |
haftmann <none@none> |
replaced slightly odd locale congruent by plain definition
|
| #
18b15cec |
|
29-Nov-2010 |
haftmann <none@none> |
equivI has replaced equiv.intro
|
| #
360a762e |
|
28-Nov-2010 |
haftmann <none@none> |
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
more natural deduction rules;
replaced slightly odd locale equiv by plain definition
|
| #
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
| #
665371e2 |
|
11-Mar-2010 |
haftmann <none@none> |
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
|
| #
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
bb2d682e |
|
02-Mar-2009 |
nipkow <none@none> |
name changes
|
| #
2f8489b9 |
|
28-Jan-2009 |
haftmann <none@none> |
Plain, Main form meeting points in import hierarchy
|
| #
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
| #
8b34ba5a |
|
16-Sep-2008 |
haftmann <none@none> |
dropped superfluous code lemmas
|
| #
34e8c667 |
|
07-May-2008 |
berghofe <none@none> |
Instantiated subst rule to avoid problems with HO unification.
|
| #
083d7485 |
|
28-Nov-2007 |
haftmann <none@none> |
dropped implicit assumption proof
|
| #
c65e27dd |
|
26-Sep-2007 |
haftmann <none@none> |
moved Finite_Set before Datatype
|
| #
698f1f55 |
|
10-Jul-2007 |
haftmann <none@none> |
moved finite lemmas to Finite_Set.thy
|
| #
4fee069a |
|
10-Dec-2006 |
wenzelm <none@none> |
respects2: tuned spacing;
|
| #
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
| #
d51ce246 |
|
03-Jul-2006 |
nipkow <none@none> |
replaced translation by abbreviation
|
| #
b5d7d8ec |
|
08-Apr-2006 |
wenzelm <none@none> |
refined 'abbreviation';
|
| #
84161ae1 |
|
23-Mar-2006 |
nipkow <none@none> |
Converted translations to abbbreviations.
Removed a few odd functions from Map and AssocList.
Moved chg_map from Map to Bali/Basis.
|
| #
d812e8a8 |
|
22-Dec-2005 |
nipkow <none@none> |
more lemmas
|
| #
d955c79b |
|
22-Dec-2005 |
nipkow <none@none> |
new lemmas
|
| #
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
| #
6d9b3eb2 |
|
21-Feb-2005 |
nipkow <none@none> |
comprehensive cleanup, replacing sumr by setsum
|
| #
4fe6092b |
|
09-Dec-2004 |
nipkow <none@none> |
First step in reorganizing Finite_Set
|
| #
3f348152 |
|
21-Nov-2004 |
nipkow <none@none> |
added lemmas
|
| #
71f87ec4 |
|
20-Nov-2004 |
nipkow <none@none> |
Restructured List and added "rotate"
|
| #
0d6498ba |
|
19-Nov-2004 |
paulson <none@none> |
moved and renamed Integ/Equiv.thy
|