2018-03-26 |
Manuel Eberl |
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
|
file |
diff |
annotate
|
2018-03-12 |
Manuel Eberl |
Changes to complete distributive lattices due to Viorel Preoteasa
|
file |
diff |
annotate
|
2018-01-10 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
2017-11-26 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2017-07-02 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
2017-06-05 |
haftmann |
modernized (code) setup for enumeration predicates
|
file |
diff |
annotate
|
2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
2016-01-01 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-05-01 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-09-16 |
blanchet |
added 'extraction' plugins -- this might help 'HOL-Proofs'
|
file |
diff |
annotate
|
2014-09-14 |
blanchet |
disable datatype 'plugins' for internal types
|
file |
diff |
annotate
|
2014-09-11 |
blanchet |
updated news
|
file |
diff |
annotate
|
2014-09-02 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
2014-05-04 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
2014-03-19 |
haftmann |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
file |
diff |
annotate
|
2014-03-18 |
haftmann |
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
|
file |
diff |
annotate
|
2014-03-16 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
2014-03-15 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
2014-02-14 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
2013-09-27 |
Andreas Lochbihler |
prefer Code.abort over code_abort
|
file |
diff |
annotate
|
2013-09-02 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
2013-02-15 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
2013-02-14 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
2013-02-14 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
2012-04-06 |
haftmann |
abandoned almost redundant *_foldr lemmas
|
file |
diff |
annotate
|
2012-03-12 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
2012-02-24 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
2012-02-24 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
2012-02-24 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
2012-02-23 |
haftmann |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
file |
diff |
annotate
|
2012-02-21 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
2012-02-19 |
haftmann |
distributed lattice properties of predicates to places of instantiation
|
file |
diff |
annotate
|
2012-01-11 |
berghofe |
Added inf_Int_eq to pred_set_conv database as well
|
file |
diff |
annotate
|
2012-01-10 |
berghofe |
Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules
|
file |
diff |
annotate
|
2011-12-29 |
haftmann |
conversions from sets to predicates and vice versa; extensionality on predicates
|
file |
diff |
annotate
|
2011-12-24 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
2011-11-25 |
wenzelm |
proper intro? declarations -- NB: elim? indexes on major premise, which is too flexible here and easily leads to inefficiences (cf. a0336f8b6558);
|
file |
diff |
annotate
|
2011-09-14 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
2011-08-23 |
haftmann |
tuned specifications, syntax and proofs
|
file |
diff |
annotate
|
2011-08-22 |
haftmann |
tuned specifications and syntax
|
file |
diff |
annotate
|
2011-08-21 |
haftmann |
avoid pred/set mixture
|
file |
diff |
annotate
|
2011-08-04 |
haftmann |
more fine-granular instantiation
|
file |
diff |
annotate
|
2011-08-03 |
haftmann |
more specific instantiation
|
file |
diff |
annotate
|
2011-07-29 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
2011-01-14 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
2011-01-11 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
2010-12-21 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
2010-12-20 |
haftmann |
type_lifting for predicates
|
file |
diff |
annotate
|
2010-12-08 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
2010-12-08 |
haftmann |
nice syntax for lattice INFI, SUPR;
|
file |
diff |
annotate
|
2010-12-08 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
2010-11-29 |
haftmann |
moved generic definitions about relations from Quotient.thy to Predicate;
|
file |
diff |
annotate
|
2010-11-22 |
haftmann |
adhere established Collect/mem convention more closely
|
file |
diff |
annotate
|
2010-11-19 |
haftmann |
eval simp rules for predicate type, simplify primitive proofs
|
file |
diff |
annotate
|
2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
2010-08-27 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|