| 2014-02-14 |
blanchet |
2014-02-14 |
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 |
2014-02-12 |
adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'
|
file | diff | annotate |
| 2013-09-27 |
Andreas Lochbihler |
2013-09-27 |
prefer Code.abort over code_abort
|
file | diff | annotate |
| 2013-09-03 |
wenzelm |
2013-09-03 |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file | diff | annotate |
| 2013-02-15 |
haftmann |
2013-02-15 |
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
|
file | diff | annotate |
| 2013-02-14 |
haftmann |
2013-02-14 |
reform of predicate compiler / quickcheck theories:
implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers!
avoid odd New_ prefix by joining related theories;
avoid overcompact name DSequence;
separated predicate inside random monad into separate theory;
consolidated name of theory Quickcheck
|
file | diff | annotate |
| 2013-02-14 |
haftmann |
2013-02-14 |
abandoned theory Plain
|
file | diff | annotate |
| 2012-04-06 |
haftmann |
2012-04-06 |
abandoned almost redundant *_foldr lemmas
|
file | diff | annotate |
| 2012-03-12 |
noschinl |
2012-03-12 |
tuned proofs
|
file | diff | annotate |
| 2012-02-24 |
haftmann |
2012-02-24 |
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 |
2012-02-24 |
given up disfruitful branch
|
file | diff | annotate |
| 2012-02-24 |
haftmann |
2012-02-24 |
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 |
2012-02-23 |
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 |
2012-02-21 |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file | diff | annotate |
| 2012-02-19 |
haftmann |
2012-02-19 |
distributed lattice properties of predicates to places of instantiation
|
file | diff | annotate |
| 2012-01-12 |
berghofe |
2012-01-12 |
Added inf_Int_eq to pred_set_conv database as well
|
file | diff | annotate |
| 2012-01-10 |
berghofe |
2012-01-10 |
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 |
2011-12-29 |
conversions from sets to predicates and vice versa; extensionality on predicates
|
file | diff | annotate |
| 2011-12-24 |
haftmann |
2011-12-24 |
adjusted to set/pred distinction by means of type constructor `set`
|
file | diff | annotate |
| 2011-11-25 |
wenzelm |
2011-11-25 |
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 |
2011-09-14 |
renamed Complete_Lattices lemmas, removed legacy names
|
file | diff | annotate |
| 2011-08-23 |
haftmann |
2011-08-23 |
tuned specifications, syntax and proofs
|
file | diff | annotate |
| 2011-08-22 |
haftmann |
2011-08-22 |
tuned specifications and syntax
|
file | diff | annotate |
| 2011-08-21 |
haftmann |
2011-08-21 |
avoid pred/set mixture
|
file | diff | annotate |
| 2011-08-04 |
haftmann |
2011-08-04 |
more fine-granular instantiation
|
file | diff | annotate |
| 2011-08-03 |
haftmann |
2011-08-03 |
more specific instantiation
|
file | diff | annotate |
| 2011-07-29 |
haftmann |
2011-07-29 |
tuned proofs
|
file | diff | annotate |
| 2011-01-14 |
wenzelm |
2011-01-14 |
eliminated global prems;
tuned proofs;
|
file | diff | annotate |
| 2011-01-11 |
haftmann |
2011-01-11 |
"enriched_type" replaces less specific "type_lifting"
|
file | diff | annotate |
| 2010-12-21 |
haftmann |
2010-12-21 |
tuned type_lifting declarations
|
file | diff | annotate |
| 2010-12-20 |
haftmann |
2010-12-20 |
type_lifting for predicates
|
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-11-29 |
haftmann |
2010-11-29 |
moved generic definitions about relations from Quotient.thy to Predicate;
more natural deduction rules
|
file | diff | annotate |
| 2010-11-22 |
haftmann |
2010-11-22 |
adhere established Collect/mem convention more closely
|
file | diff | annotate |
| 2010-11-19 |
haftmann |
2010-11-19 |
eval simp rules for predicate type, simplify primitive proofs
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
renamed class/constant eq to equal; tuned some instantiations
|
file | diff | annotate |
| 2010-08-23 |
blanchet |
2010-08-23 |
"no_atp" fact that leads to unsound Sledgehammer proofs
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
dropped superfluous [code del]s
|
file | diff | annotate |
| 2010-06-24 |
blanchet |
2010-06-24 |
yields ill-typed ATP/metis proofs -- raus!
|
file | diff | annotate |
| 2010-04-29 |
haftmann |
2010-04-29 |
code_reflect: specify module name directly after keyword
|
file | diff | annotate |
| 2010-04-28 |
haftmann |
2010-04-28 |
avoid code_datatype antiquotation
|
file | diff | annotate |
| 2010-04-16 |
wenzelm |
2010-04-16 |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file | diff | annotate |
| 2010-03-28 |
huffman |
2010-03-28 |
add/change some lemmas about lattices
|
file | diff | annotate |
| 2009-12-11 |
haftmann |
2009-12-11 |
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
|
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-12-04 |
haftmann |
2009-12-04 |
tuned code setup
|
file | diff | annotate |
| 2009-11-19 |
bulwahn |
2009-11-19 |
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
|
file | diff | annotate |
| 2009-11-12 |
bulwahn |
2009-11-12 |
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
|
file | diff | annotate |
| 2009-11-11 |
haftmann |
2009-11-11 |
tuned
|
file | diff | annotate |
| 2009-10-24 |
bulwahn |
2009-10-24 |
developing an executable the operator
|
file | diff | annotate |
| 2009-10-24 |
bulwahn |
2009-10-24 |
generalizing singleton with a default value
|
file | diff | annotate |
| 2009-10-24 |
bulwahn |
2009-10-24 |
moved meta_fun_cong lemma into ML-file; tuned
|
file | diff | annotate |
| 2009-10-06 |
haftmann |
2009-10-06 |
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
|
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 headings
|
file | diff | annotate |
| 2009-09-25 |
haftmann |
2009-09-25 |
merged
|
file | diff | annotate |