| Sun, 22 Feb 2009 10:22:29 +0100 |
haftmann |
formal dependency on newly emerging algorithm
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 14:49:24 +0100 |
haftmann |
reverted to old wellsorting algorithm
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 10:14:31 +0100 |
haftmann |
experimental inclusion of new wellsorting algorithm for code equations
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:18:31 +0100 |
haftmann |
do not drop arguments to 0, 1
|
file |
diff |
annotate
|
| Tue, 10 Feb 2009 14:02:45 +0100 |
blanchet |
Renamed descriptions of Nitpick (and ATP) attributes, so that they fit well with the rest of the sentence in ProofGeneral.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 12:31:36 +0100 |
blanchet |
Reintroduced nitpick_ind_intro attribute.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 10:37:59 +0100 |
blanchet |
Added Nitpick_Const_Psimp attribute, dropped the 's' in Nitpick_Const_Simps, and killed the Nitpick_Ind_Intros attribute.
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:57:47 +0100 |
blanchet |
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:40:23 +0100 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:29:11 +0100 |
haftmann |
added HOL-Base image
|
file |
diff |
annotate
|
| Mon, 15 Dec 2008 09:58:45 +0100 |
haftmann |
moved value.ML to src/Tools
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Thu, 20 Nov 2008 00:03:47 +0100 |
wenzelm |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 15:58:38 +0100 |
haftmann |
simproc for let
|
file |
diff |
annotate
|
| Tue, 28 Oct 2008 11:03:07 +0100 |
ballarin |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
file |
diff |
annotate
|
| Fri, 24 Oct 2008 17:48:34 +0200 |
haftmann |
"arbitrary" merely abbreviates undefined
|
file |
diff |
annotate
|
| Wed, 22 Oct 2008 14:15:45 +0200 |
haftmann |
code identifier namings are no longer imperative
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 07 Oct 2008 16:07:16 +0200 |
haftmann |
re-introduces axiom subst
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:31:57 +0200 |
haftmann |
polished code generator setup
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| Mon, 22 Sep 2008 23:00:15 +0200 |
berghofe |
Added setup for coherent logic prover.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:22 +0200 |
haftmann |
generic value command
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:09:20 +0200 |
haftmann |
restructured and split code serializer module
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:24:29 +0200 |
haftmann |
tuned code generator setup
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:47:18 +0200 |
krauss |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
file |
diff |
annotate
|
| Tue, 24 Jun 2008 19:43:14 +0200 |
wenzelm |
ML_Antiquote.value;
|
file |
diff |
annotate
|
| Mon, 23 Jun 2008 15:51:38 +0200 |
wenzelm |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 23:20:03 +0200 |
wenzelm |
removed obsolete case_split_tac -- cannot work without;
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 19:15:19 +0200 |
wenzelm |
eliminated obsolete case_split_thm -- use case_split;
|
file |
diff |
annotate
|