2016-12-21 |
haftmann |
dropped aliasses
|
file |
diff |
annotate
|
2016-10-01 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2016-09-18 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
2016-08-05 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-07-31 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-05-23 |
wenzelm |
proper document source;
|
file |
diff |
annotate
|
2016-05-23 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-05-17 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
2016-05-12 |
haftmann |
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
|
file |
diff |
annotate
|
2015-12-28 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
2015-12-27 |
wenzelm |
discontinued ASCII replacement syntax <*>;
|
file |
diff |
annotate
|
2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
2015-10-13 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
2015-10-06 |
wenzelm |
fewer aliases for toplevel theorem statements;
|
file |
diff |
annotate
|
2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-06-17 |
paulson |
New WF theorem by Tjark Weber. Replaced the proof of the subsequent theorem.
|
file |
diff |
annotate
|
2015-04-27 |
nipkow |
new lemma
|
file |
diff |
annotate
|
2015-03-25 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-10-07 |
wenzelm |
more bibtex entries;
|
file |
diff |
annotate
|
2014-04-23 |
blanchet |
move size hooks together, with new one preceding old one and sharing same theory data
|
file |
diff |
annotate
|
2014-04-03 |
blanchet |
use same idiom as used for datatype 'size' function to name constants and theorems emerging from various type interpretations -- reduces the chances of name clashes on theory merges
|
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-16 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
2014-03-06 |
blanchet |
renamed 'map_pair' to 'map_prod'
|
file |
diff |
annotate
|
2014-01-17 |
blanchet |
folded 'Wellfounded_More_FP' into 'Wellfounded'
|
file |
diff |
annotate
|
2013-11-10 |
haftmann |
qualifed popular user space names
|
file |
diff |
annotate
|
2012-10-20 |
bulwahn |
adjusting proofs
|
file |
diff |
annotate
|
2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
2012-04-03 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
2012-03-12 |
noschinl |
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
|
file |
diff |
annotate
|
2012-03-12 |
noschinl |
tuned simpset
|
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-23 |
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-01-30 |
bulwahn |
adding code_unfold to make measure executable
|
file |
diff |
annotate
|
2012-01-28 |
bulwahn |
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
|
file |
diff |
annotate
|
2012-01-25 |
bulwahn |
adding very basic code generation to Wellfounded theory
|
file |
diff |
annotate
|
2012-01-10 |
berghofe |
pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules
|
file |
diff |
annotate
|
2011-12-24 |
haftmann |
adjusted to set/pred distinction by means of type constructor `set`
|
file |
diff |
annotate
|
2011-10-13 |
haftmann |
moved acyclic predicate up in hierarchy
|
file |
diff |
annotate
|
2011-10-13 |
haftmann |
modernized definitions
|
file |
diff |
annotate
|
2011-09-20 |
haftmann |
tuned specification and lemma distribution among theories; tuned proofs
|
file |
diff |
annotate
|
2011-09-15 |
hoelzl |
removed further legacy rules from Complete_Lattices
|
file |
diff |
annotate
|
2011-09-14 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
2011-08-11 |
krauss |
removed unused material, which does not really belong here
|
file |
diff |
annotate
|
2011-06-01 |
nipkow |
tuned lemmas
|
file |
diff |
annotate
|
2011-06-01 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
2011-02-08 |
nipkow |
added termination lemmas
|
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-18 |
haftmann |
map_pair replaces prod_fun
|
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-07-12 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
2010-06-11 |
haftmann |
declare lex_prod_def [code del]
|
file |
diff |
annotate
|
2010-05-04 |
krauss |
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
|
file |
diff |
annotate
|
2010-05-04 |
haftmann |
locale predicates of classes carry a mandatory "class" prefix
|
file |
diff |
annotate
|
2010-03-18 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
2010-03-11 |
haftmann |
Big_Operators now in Main rather than Plain
|
file |
diff |
annotate
|
2010-03-10 |
haftmann |
split off theory Big_Operators from theory Finite_Set
|
file |
diff |
annotate
|
2010-02-18 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|