haftmann [Sat, 09 May 2009 09:17:45 +0200] rev 31083
merged
haftmann [Sat, 09 May 2009 09:17:29 +0200] rev 31082
interface changes in linarith.ML
nipkow [Sat, 09 May 2009 07:25:45 +0200] rev 31081
merged
nipkow [Sat, 09 May 2009 07:25:22 +0200] rev 31080
lemmas by Andreas Lochbihler
nipkow [Fri, 08 May 2009 19:20:00 +0200] rev 31079
merged
nipkow [Fri, 08 May 2009 08:07:05 +0200] rev 31078
merged
nipkow [Fri, 08 May 2009 08:06:43 +0200] rev 31077
more lemmas
huffman [Fri, 08 May 2009 16:19:51 -0700] rev 31076
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
chaieb [Fri, 08 May 2009 19:28:11 +0100] rev 31075
fixed theorem statement
chaieb [Fri, 08 May 2009 14:03:24 +0100] rev 31074
merged
chaieb [Fri, 08 May 2009 14:02:33 +0100] rev 31073
Generalized distributivity theorems of radicals over multiplication, division and inverses
haftmann [Fri, 08 May 2009 13:38:21 +0200] rev 31072
proper structure name
haftmann [Fri, 08 May 2009 13:34:27 +0200] rev 31071
localized (complete) partial order classes
haftmann [Fri, 08 May 2009 10:59:11 +0200] rev 31070
dropped legacy ml theorem binding
haftmann [Fri, 08 May 2009 09:48:54 +0200] rev 31069
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann [Fri, 08 May 2009 09:48:07 +0200] rev 31068
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann [Fri, 08 May 2009 08:01:09 +0200] rev 31067
generalized simproc for mod
haftmann [Fri, 08 May 2009 08:00:13 +0200] rev 31066
explicit method linarith
haftmann [Fri, 08 May 2009 08:00:11 +0200] rev 31065
moved int_factor_simprocs.ML to theory Int
haftmann [Thu, 07 May 2009 16:22:35 +0200] rev 31064
treat frees driectly by the LCF kernel
haftmann [Thu, 07 May 2009 16:22:35 +0200] rev 31063
dropped explicit suppport for frees in evaluation conversion stack
haftmann [Thu, 07 May 2009 16:22:34 +0200] rev 31062
no need for explicit delete declaration
haftmann [Thu, 07 May 2009 16:22:34 +0200] rev 31061
better to have distinguished class for preorders
haftmann [Thu, 07 May 2009 12:17:17 +0200] rev 31060
added theory for explicit equivalence relation in preorders
haftmann [Thu, 07 May 2009 12:02:16 +0200] rev 31059
explicit type_name antiquotations
haftmann [Thu, 07 May 2009 12:02:15 +0200] rev 31058
explicit type arguments in constants
haftmann [Wed, 06 May 2009 19:42:27 +0200] rev 31057
merged
haftmann [Wed, 06 May 2009 19:09:31 +0200] rev 31056
robustifed infrastructure for complex term syntax during code generation
haftmann [Wed, 06 May 2009 19:09:31 +0200] rev 31055
proper structures for list and string code generation stuff
haftmann [Wed, 06 May 2009 19:09:14 +0200] rev 31054
explicit type arguments in constants
haftmann [Wed, 06 May 2009 19:09:14 +0200] rev 31053
confine term setup to Eval serialiser
haftmann [Wed, 06 May 2009 16:10:12 +0200] rev 31052
adaptation replaces adaption
haftmann [Wed, 06 May 2009 16:01:23 +0200] rev 31051
refined HOL string theories and corresponding ML fragments
haftmann [Wed, 06 May 2009 16:01:07 +0200] rev 31050
adaptation replaces adaption
haftmann [Wed, 06 May 2009 16:01:06 +0200] rev 31049
explicit type arguments in constants
haftmann [Wed, 06 May 2009 16:01:06 +0200] rev 31048
refined HOL string theories and corresponding ML fragments
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