| 2011-09-13 |
noschinl |
2011-09-13 |
tune simpset for Complete_Lattices
|
file | diff | annotate |
| 2011-09-09 |
krauss |
2011-09-09 |
added syntactic classes for "inf" and "sup"
|
file | diff | annotate |
| 2011-08-08 |
haftmann |
2011-08-08 |
move legacy candiates to bottom; marked candidates for default simp rules
|
file | diff | annotate |
| 2011-07-17 |
haftmann |
2011-07-17 |
more on complement
|
file | diff | annotate |
| 2011-07-10 |
haftmann |
2011-07-10 |
tuned notation
|
file | diff | annotate |
| 2010-12-08 |
haftmann |
2010-12-08 |
bot comes before top, inf before sup etc.
|
file | diff | annotate |
| 2010-12-08 |
haftmann |
2010-12-08 |
nice syntax for lattice INFI, SUPR;
various *_apply rules for lattice operations on fun;
more default simplification rules
|
file | diff | annotate |
| 2010-12-08 |
haftmann |
2010-12-08 |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
dropped superfluous [code del]s
|
file | diff | annotate |
| 2010-05-05 |
haftmann |
2010-05-05 |
tuned whitespace
|
file | diff | annotate |
| 2010-05-04 |
haftmann |
2010-05-04 |
locale predicates of classes carry a mandatory "class" prefix
|
file | diff | annotate |
| 2010-04-26 |
Cezary Kaliszyk |
2010-04-26 |
add bounded_lattice_bot and bounded_lattice_top type classes
|
file | diff | annotate |
| 2010-04-07 |
ballarin |
2010-04-07 |
Merged resolving conflicts NEWS and locale.ML.
|
file | diff | annotate |
| 2010-02-15 |
ballarin |
2010-02-15 |
Tuned interpretation proofs.
|
file | diff | annotate |
| 2010-03-28 |
huffman |
2010-03-28 |
add/change some lemmas about lattices
|
file | diff | annotate |
| 2010-03-11 |
haftmann |
2010-03-11 |
fixed typo
|
file | diff | annotate |
| 2010-02-22 |
haftmann |
2010-02-22 |
distributed theory Algebras to theories Groups and Lattices
|
file | diff | annotate |
| 2010-02-12 |
haftmann |
2010-02-12 |
tuned import order
|
file | diff | annotate |
| 2010-02-05 |
haftmann |
2010-02-05 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| 2010-01-28 |
haftmann |
2010-01-28 |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file | diff | annotate |
| 2009-12-30 |
krauss |
2009-12-30 |
killed a few warnings
|
file | diff | annotate |
| 2009-12-05 |
haftmann |
2009-12-05 |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file | diff | annotate |
| 2009-09-30 |
haftmann |
2009-09-30 |
moved lemmas about sup on bool to Lattices.thy
|
file | diff | annotate |
| 2009-09-30 |
haftmann |
2009-09-30 |
tuned proofs
|
file | diff | annotate |
| 2009-09-22 |
haftmann |
2009-09-22 |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file | diff | annotate |
| 2009-09-14 |
haftmann |
2009-09-14 |
some lemmas about strict order in lattices
|
file | diff | annotate |
| 2009-09-03 |
haftmann |
2009-09-03 |
proper class syntax for sublocale class < expr
|
file | diff | annotate |
| 2009-08-28 |
nipkow |
2009-08-28 |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
file | diff | annotate |
| 2009-07-25 |
haftmann |
2009-07-25 |
localized interpretation of min/max-lattice
|
file | diff | annotate |
| 2009-07-14 |
haftmann |
2009-07-14 |
refinement of lattice classes
|
file | diff | annotate |
| 2009-07-13 |
haftmann |
2009-07-13 |
removed outdated comment
|
file | diff | annotate |
| 2009-07-11 |
haftmann |
2009-07-11 |
added boolean_algebra type class; tuned lattice duals
|
file | diff | annotate |
| 2009-03-26 |
wenzelm |
2009-03-26 |
interpretation/interpret: prefixes are mandatory by default;
|
file | diff | annotate |
| 2009-03-05 |
haftmann |
2009-03-05 |
moved complete_lattice to Set.thy
|
file | diff | annotate |
| 2009-01-21 |
haftmann |
2009-01-21 |
dropped ID
|
file | diff | annotate |
| 2009-01-16 |
haftmann |
2009-01-16 |
migrated class package to new locale implementation
|
file | diff | annotate |
| 2008-12-11 |
ballarin |
2008-12-11 |
Conversion of HOL-Main and ZF to new locales.
|
file | diff | annotate |
| 2008-11-17 |
haftmann |
2008-11-17 |
tuned unfold_locales invocation
|
file | diff | annotate |
| 2008-10-27 |
haftmann |
2008-10-27 |
sup_bot and inf_top
|
file | diff | annotate |
| 2008-10-24 |
haftmann |
2008-10-24 |
new classes "top" and "bot"
|
file | diff | annotate |
| 2008-10-10 |
haftmann |
2008-10-10 |
`code func` now just `code`
|
file | diff | annotate |
| 2008-07-25 |
haftmann |
2008-07-25 |
added class preorder
|
file | diff | annotate |
| 2008-05-07 |
berghofe |
2008-05-07 |
- 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.
|
file | diff | annotate |
| 2008-03-07 |
haftmann |
2008-03-07 |
tuned proofs
|
file | diff | annotate |
| 2008-01-30 |
haftmann |
2008-01-30 |
dual orders and dual lattices
|
file | diff | annotate |
| 2007-11-30 |
haftmann |
2007-11-30 |
adjustions to due to instance target
|
file | diff | annotate |
| 2007-11-28 |
haftmann |
2007-11-28 |
dropped implicit assumption proof
|
file | diff | annotate |
| 2007-11-10 |
wenzelm |
2007-11-10 |
tuned specifications of 'notation';
|
file | diff | annotate |
| 2007-10-26 |
haftmann |
2007-10-26 |
localized monotonicity; tuned syntax
|
file | diff | annotate |
| 2007-10-19 |
haftmann |
2007-10-19 |
antisymmetry not a default intro rule any longer
|
file | diff | annotate |
| 2007-10-16 |
haftmann |
2007-10-16 |
global class syntax
|
file | diff | annotate |
| 2007-09-29 |
haftmann |
2007-09-29 |
further localization
|
file | diff | annotate |
| 2007-09-18 |
ballarin |
2007-09-18 |
Simplified proofs due to transitivity reasoner setup.
|
file | diff | annotate |
| 2007-09-01 |
wenzelm |
2007-09-01 |
mono_Int/Un: proper proof, avoid illegal schematic type vars;
removed obsolete ML bindings;
|
file | diff | annotate |
| 2007-08-20 |
haftmann |
2007-08-20 |
Sup now explicit parameter of complete_lattice
|
file | diff | annotate |
| 2007-08-07 |
haftmann |
2007-08-07 |
tuned
|
file | diff | annotate |
| 2007-07-24 |
haftmann |
2007-07-24 |
using class target
|
file | diff | annotate |
| 2007-07-20 |
haftmann |
2007-07-20 |
simplified HOL bootstrap
|
file | diff | annotate |
| 2007-06-14 |
wenzelm |
2007-06-14 |
tuned proofs: avoid implicit prems;
|
file | diff | annotate |
| 2007-05-24 |
haftmann |
2007-05-24 |
rudimentary class target implementation
|
file | diff | annotate |