haftmann [Wed, 06 May 2009 16:01:05 +0200] rev 31047
tuned description of overloading
haftmann [Wed, 06 May 2009 16:01:05 +0200] rev 31046
confine term setup to Eval serialiser
haftmann [Wed, 06 May 2009 16:01:05 +0200] rev 31045
updated generated file
nipkow [Wed, 06 May 2009 19:15:40 +0200] rev 31044
new lemmas
nipkow [Wed, 06 May 2009 09:58:24 +0200] rev 31043
merged
Timothy Bourke [Wed, 06 May 2009 10:55:47 +1000] rev 31042
Prototype introiff option for find_theorems.
This feature was suggested by Jeremy Avigad / Tobias Nipkow.
It adds an introiff keyword for find_theorems that returns, in
addition to the usual results for intro, any theorems of the
form ([| ... |] ==> (P = Q)) where either P or Q matches the
conclusions of the current goal. Such theorems can be made
introduction rules with [THEN iffDx].
The current patch is for evaluation only. It assumes an
(op = : 'a -> 'a -> bool) operator, which is specific to HOL.
It is not clear how this should be generalised.
huffman [Wed, 06 May 2009 00:57:29 -0700] rev 31041
replace cont2cont_apply with cont_apply; add new cont2cont lemmas
haftmann [Wed, 06 May 2009 09:08:47 +0200] rev 31040
compatible with preorder; bot and top instances
immler@in.tum.de [Mon, 04 May 2009 23:45:58 +0200] rev 31039
updated generated files etc/isar-keywords.el and lib/jedit/isabelle.xml
immler@in.tum.de [Mon, 04 May 2009 23:44:11 +0200] rev 31038
tuned
immler@in.tum.de [Mon, 04 May 2009 23:37:39 +0200] rev 31037
added Philipp Meyer's implementation of AtpMinimal
together with related changes in the sledgehammer-interface:
adapted type of prover, optional relevance filtering,
public get_prover for registered atps in AtpManager,
included atp_minimize in s/h response;
haftmann [Mon, 04 May 2009 14:49:51 +0200] rev 31036
removed code_name module
haftmann [Mon, 04 May 2009 14:49:50 +0200] rev 31035
desymbolization with case selection
haftmann [Mon, 04 May 2009 14:49:49 +0200] rev 31034
dropped duplicate lemma sum_nonneg_eq_zero_iff
haftmann [Mon, 04 May 2009 14:49:48 +0200] rev 31033
fixed broken link
haftmann [Mon, 04 May 2009 14:49:47 +0200] rev 31032
tuned header
haftmann [Mon, 04 May 2009 14:49:46 +0200] rev 31031
class typerep inherits from type
huffman [Thu, 30 Apr 2009 14:46:59 -0700] rev 31030
use simproc_setup command for cont_proc
huffman [Thu, 30 Apr 2009 12:16:35 -0700] rev 31029
used named theorems for declaring numeral simps
huffman [Thu, 30 Apr 2009 11:14:04 -0700] rev 31028
clean up unsigned numeral proofs
huffman [Thu, 30 Apr 2009 07:33:40 -0700] rev 31027
detect error cases in mk_num, dest_num
huffman [Wed, 29 Apr 2009 20:33:52 -0700] rev 31026
add semiring_assoc_fold simproc for unsigned numerals
huffman [Wed, 29 Apr 2009 17:57:16 -0700] rev 31025
reorient simproc for unsigned numerals
huffman [Wed, 29 Apr 2009 17:15:01 -0700] rev 31024
reimplement reorientation simproc using theory data
huffman [Wed, 29 Apr 2009 13:36:29 -0700] rev 31023
use opaque ascription for all HOLCF code
nipkow [Wed, 29 Apr 2009 21:10:46 +0200] rev 31022
added listsum lemmas
haftmann [Wed, 29 Apr 2009 14:20:26 +0200] rev 31021
farewell to class recpower
haftmann [Tue, 28 Apr 2009 19:15:50 +0200] rev 31020
merged
haftmann [Tue, 28 Apr 2009 16:58:23 +0200] rev 31019
power constraint needed, though
haftmann [Tue, 28 Apr 2009 15:50:32 +0200] rev 31018
stripped lemma duplicatesrc/HOL/Word/Num_Lemmas.thy