| Sat, 07 Mar 2009 17:05:40 +0100 |
blanchet |
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 15:31:07 +0100 |
blanchet |
Added a "nitpick_maybe" symbol, which is used by Nitpick. This will go away once Nitpick is part of HOL.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 18:18:05 +0100 |
blanchet |
Second try at adding "nitpick_const_def" attribute.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 18:40:16 +0100 |
blanchet |
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
|
file |
diff |
annotate
|
| Mon, 02 Mar 2009 16:58:39 +0100 |
haftmann |
reduced confusion code_funcgr vs. code_wellsorted
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:52:21 +0100 |
wenzelm |
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
|
file |
diff |
annotate
|
| Sat, 28 Feb 2009 14:02:12 +0100 |
wenzelm |
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
|
file |
diff |
annotate
|
| Sun, 22 Feb 2009 22:32:50 +0100 |
haftmann |
experimental switch to new well-sorting algorithm
|
file |
diff |
annotate
|
| 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
|
| Tue, 10 Jun 2008 15:30:58 +0200 |
haftmann |
localized Least in Orderings.thy
|
file |
diff |
annotate
|
| Sun, 18 May 2008 17:03:20 +0200 |
wenzelm |
eliminated theory CPure;
|
file |
diff |
annotate
|
| Thu, 24 Apr 2008 16:53:04 +0200 |
haftmann |
moved 'trivial classes' to foundation of code generator
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 22:00:25 +0200 |
haftmann |
different handling of eq class for nbe
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:13 +0200 |
wenzelm |
Sign.hide_const;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2008 18:30:40 +0200 |
krauss |
Generic conversion and tactic "atomize_elim" to convert elimination rules
|
file |
diff |
annotate
|
| Fri, 04 Apr 2008 13:40:21 +0200 |
haftmann |
postprocessing of equality
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:01 +0100 |
wenzelm |
pass imp_elim, swap to classical prover;
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Sat, 22 Dec 2007 14:10:22 +0100 |
wenzelm |
use random_word.ML earlier;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:44:18 +0100 |
wenzelm |
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:33 +0100 |
haftmann |
interpretation of typedecls: instantiation to class type
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:00:05 +0100 |
wenzelm |
tuned specifications of 'notation';
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 22:50:00 +0100 |
kleing |
move itself into HOL types
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|