| Thu, 04 Aug 2011 20:11:39 +0200 |
haftmann |
more fine-granular instantiation
|
file |
diff |
annotate
|
| Wed, 03 Aug 2011 23:21:53 +0200 |
haftmann |
more specific instantiation
|
file |
diff |
annotate
|
| Fri, 29 Jul 2011 19:47:55 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 15:37:25 +0100 |
haftmann |
type_lifting for predicates
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 15:05:46 +0100 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 14:52:23 +0100 |
haftmann |
nice syntax for lattice INFI, SUPR;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 12:14:46 +0100 |
haftmann |
moved generic definitions about relations from Quotient.thy to Predicate;
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 17:48:35 +0100 |
haftmann |
adhere established Collect/mem convention more closely
|
file |
diff |
annotate
|
| Fri, 19 Nov 2010 14:35:58 +0100 |
haftmann |
eval simp rules for predicate type, simplify primitive proofs
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 14:51:56 +0200 |
blanchet |
"no_atp" fact that leads to unsound Sledgehammer proofs
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 21:01:13 +0200 |
blanchet |
yields ill-typed ATP/metis proofs -- raus!
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:56:18 +0200 |
haftmann |
avoid code_datatype antiquotation
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 12:49:14 -0700 |
huffman |
add/change some lemmas about lattices
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 14:43:56 +0100 |
haftmann |
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 20:02:21 +0100 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:19:30 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:53 +0100 |
bulwahn |
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:37 +0100 |
bulwahn |
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 09:02:20 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
developing an executable the operator
|
file |
diff |
annotate
|