#
936f4b2b |
|
17-Nov-2019 |
haftmann <none@none> |
strengthened type class for bit operations
|
#
0dca4c19 |
|
03-Nov-2019 |
wenzelm <none@none> |
tuned whitespace;
|
#
7625757f |
|
07-Aug-2019 |
wenzelm <none@none> |
prefer named lemmas -- more compact proofterms;
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
78eb1fe1 |
|
25-Feb-2018 |
immler <none@none> |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
58b13a3d |
|
07-Sep-2016 |
haftmann <none@none> |
discontinued theory-local special syntax for lattice orderings --HG-- extra : rebase_source : a43595e983fb7b5e8e9031a09ddee560d27e761b
|
#
ee790de8 |
|
10-Aug-2016 |
haftmann <none@none> |
formal passive interpretation proofs for conj and disj --HG-- extra : rebase_source : 2435eb0e495ed87fe580548ef966997d83f05541
|
#
f937778a |
|
02-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
eab922d6 |
|
20-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
0522687a |
|
11-Jun-2016 |
haftmann <none@none> |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes --HG-- extra : rebase_source : 4542f54b0b7fe6c0bea5be2116706e4cfacadaf0
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
2033ce77 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
cancel complementary terms as arguments to sup/inf in boolean algebras
|
#
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
40037c93 |
|
15-Feb-2015 |
haftmann <none@none> |
explicit equivalence for strict order on lattices
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
ab986fd1 |
|
25-Dec-2013 |
haftmann <none@none> |
explicit distributivity facts on min/max
|
#
4a7fe805 |
|
25-Dec-2013 |
haftmann <none@none> |
postponed min/max lemmas until abstract lattice is available
|
#
f3bdee62 |
|
25-Dec-2013 |
haftmann <none@none> |
prefer abstract simp rule
|
#
ae5ba0b5 |
|
25-Dec-2013 |
haftmann <none@none> |
more lemmas on abstract lattices
|
#
f71fdda3 |
|
24-Dec-2013 |
haftmann <none@none> |
tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs
|
#
f55a6e4d |
|
21-Nov-2013 |
blanchet <none@none> |
rationalize imports
|
#
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
#
0da1300b |
|
26-May-2013 |
haftmann <none@none> |
examples for interpretation into target
|
#
45720e9d |
|
01-Apr-2013 |
nipkow <none@none> |
added lemma
|
#
eda70abb |
|
26-Mar-2013 |
haftmann <none@none> |
more uniform style for interpretation and sublocale declarations --HG-- extra : rebase_source : 908fa43d5ac738a6c353d74475cb1910f6a318e8
|
#
de37771f |
|
26-Mar-2013 |
haftmann <none@none> |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
#
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
#
a187bec2 |
|
23-Mar-2013 |
haftmann <none@none> |
locales for abstract orders
|
#
43e69fef |
|
10-Mar-2013 |
nipkow <none@none> |
stepwise instantiation is more modular
|
#
f405b09c |
|
21-Dec-2012 |
nipkow <none@none> |
added simp rule
|
#
dee31516 |
|
09-Oct-2012 |
haftmann <none@none> |
more explicit code equations
|
#
81c2aa38 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned proofs
|
#
f9af5d85 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned simpset
|
#
92c9b3bf |
|
26-Feb-2012 |
haftmann <none@none> |
tuned syntax declarations; tuned structure --HG-- extra : rebase_source : 1b6c21e91abe00bbf0ca93b6c0f5a24da0bef488
|
#
1cc410e1 |
|
26-Feb-2012 |
haftmann <none@none> |
marked candidates for rule declarations
|
#
f0c3a8ae |
|
23-Feb-2012 |
haftmann <none@none> |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
#
98c01e6d |
|
21-Feb-2012 |
haftmann <none@none> |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
#
a8fde5da |
|
19-Feb-2012 |
haftmann <none@none> |
distributed lattice properties of predicates to places of instantiation --HG-- extra : rebase_source : f060e45b06e82cc14c73eba231a21e4636bbe179
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
551d75e2 |
|
13-Sep-2011 |
noschinl <none@none> |
tune proofs
|
#
a3372eca |
|
13-Sep-2011 |
noschinl <none@none> |
tune simpset for Complete_Lattices
|
#
1947c572 |
|
08-Sep-2011 |
krauss <none@none> |
added syntactic classes for "inf" and "sup"
|
#
922a31a8 |
|
08-Aug-2011 |
haftmann <none@none> |
move legacy candiates to bottom; marked candidates for default simp rules
|
#
4d2ca5ff |
|
17-Jul-2011 |
haftmann <none@none> |
more on complement
|
#
7eb69ed4 |
|
10-Jul-2011 |
haftmann <none@none> |
tuned notation
|
#
5531c3e2 |
|
08-Dec-2010 |
haftmann <none@none> |
bot comes before top, inf before sup etc.
|
#
4b2fbf2e |
|
08-Dec-2010 |
haftmann <none@none> |
nice syntax for lattice INFI, SUPR; various *_apply rules for lattice operations on fun; more default simplification rules
|
#
ce4d56f1 |
|
08-Dec-2010 |
haftmann <none@none> |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
7842b27b |
|
05-May-2010 |
haftmann <none@none> |
tuned whitespace
|
#
4f324f64 |
|
04-May-2010 |
haftmann <none@none> |
locale predicates of classes carry a mandatory "class" prefix
|
#
646583b8 |
|
26-Apr-2010 |
Cezary Kaliszyk <kaliszyk@in.tum.de> |
add bounded_lattice_bot and bounded_lattice_top type classes
|
#
987c82fb |
|
28-Mar-2010 |
huffman <none@none> |
add/change some lemmas about lattices
|
#
0053a79a |
|
11-Mar-2010 |
haftmann <none@none> |
fixed typo
|
#
836163e7 |
|
22-Feb-2010 |
haftmann <none@none> |
distributed theory Algebras to theories Groups and Lattices
|
#
05a98919 |
|
14-Feb-2010 |
ballarin <none@none> |
Tuned interpretation proofs.
|
#
c0fe55ae |
|
12-Feb-2010 |
haftmann <none@none> |
tuned import order
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
761011a7 |
|
28-Jan-2010 |
haftmann <none@none> |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
#
6cb03d83 |
|
30-Dec-2009 |
krauss <none@none> |
killed a few warnings
|
#
496367cb |
|
05-Dec-2009 |
haftmann <none@none> |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
#
bc072ffb |
|
30-Sep-2009 |
haftmann <none@none> |
moved lemmas about sup on bool to Lattices.thy
|
#
e47d59e1 |
|
30-Sep-2009 |
haftmann <none@none> |
tuned proofs
|
#
122eebc6 |
|
22-Sep-2009 |
haftmann <none@none> |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
#
2f44608c |
|
14-Sep-2009 |
haftmann <none@none> |
some lemmas about strict order in lattices
|
#
2d2bc6cd |
|
03-Sep-2009 |
haftmann <none@none> |
proper class syntax for sublocale class < expr
|
#
a5900588 |
|
28-Aug-2009 |
nipkow <none@none> |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
#
ea56e793 |
|
25-Jul-2009 |
haftmann <none@none> |
localized interpretation of min/max-lattice
|
#
ee1f011f |
|
14-Jul-2009 |
haftmann <none@none> |
refinement of lattice classes
|
#
b5309952 |
|
13-Jul-2009 |
haftmann <none@none> |
removed outdated comment
|
#
822ce3cc |
|
11-Jul-2009 |
haftmann <none@none> |
added boolean_algebra type class; tuned lattice duals
|
#
0761d736 |
|
26-Mar-2009 |
wenzelm <none@none> |
interpretation/interpret: prefixes are mandatory by default;
|
#
81fb684d |
|
05-Mar-2009 |
haftmann <none@none> |
moved complete_lattice to Set.thy
|
#
0248177c |
|
21-Jan-2009 |
haftmann <none@none> |
dropped ID
|
#
7b4d17c7 |
|
16-Jan-2009 |
haftmann <none@none> |
migrated class package to new locale implementation
|
#
6d30ce6c |
|
11-Dec-2008 |
ballarin <none@none> |
Conversion of HOL-Main and ZF to new locales.
|
#
39d5f60f |
|
17-Nov-2008 |
haftmann <none@none> |
tuned unfold_locales invocation
|
#
a243137d |
|
27-Oct-2008 |
haftmann <none@none> |
sup_bot and inf_top
|
#
46ae01f8 |
|
24-Oct-2008 |
haftmann <none@none> |
new classes "top" and "bot"
|
#
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
#
a84018cb |
|
24-Jul-2008 |
haftmann <none@none> |
added class preorder
|
#
dcf9a5a1 |
|
07-May-2008 |
berghofe <none@none> |
- Now imports Fun rather than Orderings - Moved "Set as lattice" section behind "Fun as lattice" section, since sets are just functions. - The instantiations instantiation set :: (type) distrib_lattice instantiation set :: (type) complete_lattice are no longer needed, and the former definitions inf_set_eq, sup_set_eq, Inf_set_def, and Sup_set_def can now be derived from abstract properties of sup, inf, etc.
|
#
33131daf |
|
07-Mar-2008 |
haftmann <none@none> |
tuned proofs
|
#
57623aca |
|
30-Jan-2008 |
haftmann <none@none> |
dual orders and dual lattices
|
#
afc0b201 |
|
30-Nov-2007 |
haftmann <none@none> |
adjustions to due to instance target
|
#
083d7485 |
|
28-Nov-2007 |
haftmann <none@none> |
dropped implicit assumption proof
|
#
e93ea3ee |
|
10-Nov-2007 |
wenzelm <none@none> |
tuned specifications of 'notation';
|
#
64949e78 |
|
26-Oct-2007 |
haftmann <none@none> |
localized monotonicity; tuned syntax
|
#
9d8a0196 |
|
19-Oct-2007 |
haftmann <none@none> |
antisymmetry not a default intro rule any longer
|
#
d2ad869d |
|
16-Oct-2007 |
haftmann <none@none> |
global class syntax
|
#
c204fbd6 |
|
29-Sep-2007 |
haftmann <none@none> |
further localization
|
#
d547e2bb |
|
18-Sep-2007 |
ballarin <none@none> |
Simplified proofs due to transitivity reasoner setup.
|
#
91d19876 |
|
01-Sep-2007 |
wenzelm <none@none> |
mono_Int/Un: proper proof, avoid illegal schematic type vars; removed obsolete ML bindings;
|
#
1a780cb0 |
|
20-Aug-2007 |
haftmann <none@none> |
Sup now explicit parameter of complete_lattice
|
#
dcf32be3 |
|
07-Aug-2007 |
haftmann <none@none> |
tuned
|
#
82fbd642 |
|
24-Jul-2007 |
haftmann <none@none> |
using class target
|
#
b8ec8316 |
|
20-Jul-2007 |
haftmann <none@none> |
simplified HOL bootstrap
|
#
282fc2bd |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
#
0263c30e |
|
24-May-2007 |
haftmann <none@none> |
rudimentary class target implementation
|
#
0a32d854 |
|
19-May-2007 |
haftmann <none@none> |
no special treatment in naming of locale predicates stemming form classes
|
#
8513a43b |
|
10-May-2007 |
haftmann <none@none> |
tuned
|
#
d5594bbb |
|
20-Apr-2007 |
haftmann <none@none> |
tuned
|
#
da418fa3 |
|
29-Mar-2007 |
haftmann <none@none> |
dropped legacy ML bindings
|
#
98345bb2 |
|
16-Mar-2007 |
haftmann <none@none> |
integrated with LOrder.thy
|
#
e1e12128 |
|
09-Mar-2007 |
haftmann <none@none> |
stepping towards uniform lattice theory development in HOL
|
#
4fc05970 |
|
02-Mar-2007 |
haftmann <none@none> |
prefix of class interpretation not mandatory any longer
|
#
dd3641f3 |
|
22-Jan-2007 |
nipkow <none@none> |
simplified proofs
|
#
d06ce1ce |
|
20-Jan-2007 |
wenzelm <none@none> |
tuned ML setup;
|
#
eb75a841 |
|
16-Jan-2007 |
haftmann <none@none> |
renamed locale partial_order to order
|
#
9a2defb7 |
|
10-Dec-2006 |
nipkow <none@none> |
renaming
|
#
04d897fa |
|
09-Dec-2006 |
nipkow <none@none> |
Modified lattice locale
|
#
abdacaef |
|
01-Dec-2006 |
haftmann <none@none> |
stripped some legacy bindings
|
#
c843b574 |
|
15-Nov-2006 |
haftmann <none@none> |
reworking of min/max lemmas
|
#
ff13c87f |
|
12-Nov-2006 |
nipkow <none@none> |
started reorgnization of lattice theories
|
#
349620b1 |
|
08-Nov-2006 |
haftmann <none@none> |
renamed Lattice_Locales to Lattices
|