2010-04-29 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
2010-04-28 |
haftmann |
avoid code_datatype antiquotation
|
file |
diff |
annotate
|
2010-04-16 |
wenzelm |
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 |
add/change some lemmas about lattices
|
file |
diff |
annotate
|
2009-12-11 |
haftmann |
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
|
file |
diff |
annotate
|
2009-12-05 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
2009-12-04 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
2009-11-19 |
bulwahn |
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
|
file |
diff |
annotate
|
2009-11-12 |
bulwahn |
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
|
file |
diff |
annotate
|
2009-11-11 |
haftmann |
tuned
|
file |
diff |
annotate
|
2009-10-24 |
bulwahn |
developing an executable the operator
|
file |
diff |
annotate
|
2009-10-24 |
bulwahn |
generalizing singleton with a default value
|
file |
diff |
annotate
|
2009-10-24 |
bulwahn |
moved meta_fun_cong lemma into ML-file; tuned
|
file |
diff |
annotate
|
2009-10-06 |
haftmann |
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
|
file |
diff |
annotate
|
2009-09-30 |
haftmann |
moved lemmas about sup on bool to Lattices.thy
|
file |
diff |
annotate
|
2009-09-30 |
haftmann |
tuned headings
|
file |
diff |
annotate
|
2009-09-25 |
haftmann |
merged
|
file |
diff |
annotate
|
2009-09-23 |
haftmann |
removed potentially dangerous rules from pred_set_conv
|
file |
diff |
annotate
|
2009-09-23 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
2009-09-18 |
haftmann |
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
|
file |
diff |
annotate
|
2009-09-15 |
haftmann |
hide new constants
|
file |
diff |
annotate
|
2009-09-15 |
haftmann |
added emptiness check predicate and singleton projection
|
file |
diff |
annotate
|
2009-08-14 |
haftmann |
formally stylized
|
file |
diff |
annotate
|
2009-07-27 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
2009-07-03 |
haftmann |
avoid useless code equations
|
file |
diff |
annotate
|
2009-05-21 |
haftmann |
added Predicate.map in SML environment
|
file |
diff |
annotate
|
2009-05-20 |
haftmann |
added Predicate.map
|
file |
diff |
annotate
|
2009-05-13 |
haftmann |
dropped sort constraint on predicate equality
|
file |
diff |
annotate
|
2009-05-12 |
haftmann |
added dummy values keyword
|
file |
diff |
annotate
|
2009-05-11 |
haftmann |
avoid latex output problem
|
file |
diff |
annotate
|