| Thu, 14 May 2009 15:09:48 +0200 |
merged module code_unit.ML into code.ML
|
file | diff | annotate |
| Thu, 14 May 2009 09:16:34 +0200 |
rewrite op = == eq handled by simproc
|
file | diff | annotate |
| Wed, 13 May 2009 18:41:35 +0200 |
itself is instance of eq
|
file | diff | annotate |
| Tue, 12 May 2009 19:30:33 +0200 |
transferred code generator preprocessor into separate module
|
file | diff | annotate |
| Wed, 29 Apr 2009 17:15:01 -0700 |
reimplement reorientation simproc using theory data
|
file | diff | annotate |
| Sat, 25 Apr 2009 21:28:04 +0200 |
misc cleanup of auto_solve and quickcheck:
|
file | diff | annotate |
| Fri, 24 Apr 2009 08:24:54 +0200 |
generic postprocessing scheme for term evaluations
|
file | diff | annotate |
| Thu, 23 Apr 2009 12:17:50 +0200 |
avoid local [code]
|
file | diff | annotate |
| Fri, 17 Apr 2009 14:29:56 +0200 |
re-engineering of evaluation conversions
|
file | diff | annotate |
| Wed, 15 Apr 2009 15:52:37 +0200 |
code generator bootstrap theory src/Tools/Code_Generator.thy
|
file | diff | annotate |
| Wed, 15 Apr 2009 15:34:54 +0200 |
wrecked old code_funcgr module
|
file | diff | annotate |
| Fri, 20 Mar 2009 17:12:37 +0100 |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file | diff | annotate |
| Sat, 07 Mar 2009 17:05:40 +0100 |
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
|
file | diff | annotate |
| Fri, 06 Mar 2009 15:31:07 +0100 |
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 |
Second try at adding "nitpick_const_def" attribute.
|
file | diff | annotate |
| Wed, 04 Mar 2009 11:05:29 +0100 |
Merge.
|
file | diff | annotate |
| Wed, 04 Mar 2009 10:45:52 +0100 |
Merge.
|
file | diff | annotate |
| Sun, 01 Mar 2009 18:40:16 +0100 |
Added "nitpick_const_def" attribute, for overriding the definition axiom of a constant.
|
file | diff | annotate |
| Mon, 02 Mar 2009 16:58:39 +0100 |
reduced confusion code_funcgr vs. code_wellsorted
|
file | diff | annotate |
| Sat, 28 Feb 2009 14:52:21 +0100 |
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
|
file | diff | annotate |
| Sat, 28 Feb 2009 14:02:12 +0100 |
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
|
file | diff | annotate |
| Sun, 22 Feb 2009 22:32:50 +0100 |
experimental switch to new well-sorting algorithm
|
file | diff | annotate |
| Sun, 22 Feb 2009 10:22:29 +0100 |
formal dependency on newly emerging algorithm
|
file | diff | annotate |
| Fri, 20 Feb 2009 14:49:24 +0100 |
reverted to old wellsorting algorithm
|
file | diff | annotate |
| Fri, 20 Feb 2009 10:14:31 +0100 |
experimental inclusion of new wellsorting algorithm for code equations
|
file | diff | annotate |
| Wed, 18 Feb 2009 19:18:31 +0100 |
do not drop arguments to 0, 1
|
file | diff | annotate |
| Tue, 10 Feb 2009 14:02:45 +0100 |
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 |
Reintroduced nitpick_ind_intro attribute.
|
file | diff | annotate |
| Mon, 09 Feb 2009 10:37:59 +0100 |
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 |
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
|
file | diff | annotate |
| Wed, 21 Jan 2009 23:40:23 +0100 |
no base sort in class import
|
file | diff | annotate |
| Fri, 16 Jan 2009 08:29:11 +0100 |
added HOL-Base image
|
file | diff | annotate |
| Mon, 15 Dec 2008 09:58:45 +0100 |
moved value.ML to src/Tools
|
file | diff | annotate |
| Wed, 03 Dec 2008 15:58:44 +0100 |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file | diff | annotate |
| Thu, 20 Nov 2008 00:03:47 +0100 |
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
|
file | diff | annotate |
| Thu, 13 Nov 2008 15:58:38 +0100 |
simproc for let
|
file | diff | annotate |
| Tue, 28 Oct 2008 11:03:07 +0100 |
Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
|
file | diff | annotate |
| Fri, 24 Oct 2008 17:48:34 +0200 |
"arbitrary" merely abbreviates undefined
|
file | diff | annotate |
| Wed, 22 Oct 2008 14:15:45 +0200 |
code identifier namings are no longer imperative
|
file | diff | annotate |
| Fri, 10 Oct 2008 06:45:53 +0200 |
`code func` now just `code`
|
file | diff | annotate |
| Tue, 07 Oct 2008 16:07:16 +0200 |
re-introduces axiom subst
|
file | diff | annotate |
| Mon, 29 Sep 2008 12:31:57 +0200 |
polished code generator setup
|
file | diff | annotate |
| Thu, 25 Sep 2008 09:28:03 +0200 |
discontinued special treatment of op = vs. eq_class.eq
|
file | diff | annotate |
| Mon, 22 Sep 2008 23:00:15 +0200 |
Added setup for coherent logic prover.
|
file | diff | annotate |
| Tue, 16 Sep 2008 09:21:22 +0200 |
generic value command
|
file | diff | annotate |
| Thu, 28 Aug 2008 22:09:20 +0200 |
restructured and split code serializer module
|
file | diff | annotate |
| Wed, 27 Aug 2008 11:24:29 +0200 |
tuned code generator setup
|
file | diff | annotate |
| Mon, 14 Jul 2008 17:47:18 +0200 |
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
|
file | diff | annotate |
| Tue, 24 Jun 2008 19:43:14 +0200 |
ML_Antiquote.value;
|
file | diff | annotate |
| Mon, 23 Jun 2008 15:51:38 +0200 |
moved src/HOL/Tools/induct_tacs.ML to src/Tools/induct_tacs.ML;
|
file | diff | annotate |
| Sat, 14 Jun 2008 23:20:03 +0200 |
removed obsolete case_split_tac -- cannot work without;
|
file | diff | annotate |
| Tue, 10 Jun 2008 19:15:19 +0200 |
eliminated obsolete case_split_thm -- use case_split;
|
file | diff | annotate |
| Tue, 10 Jun 2008 15:30:58 +0200 |
localized Least in Orderings.thy
|
file | diff | annotate |
| Sun, 18 May 2008 17:03:20 +0200 |
eliminated theory CPure;
|
file | diff | annotate |
| Thu, 24 Apr 2008 16:53:04 +0200 |
moved 'trivial classes' to foundation of code generator
|
file | diff | annotate |
| Tue, 22 Apr 2008 22:00:25 +0200 |
different handling of eq class for nbe
|
file | diff | annotate |
| Tue, 22 Apr 2008 08:33:16 +0200 |
constant HOL.eq now qualified
|
file | diff | annotate |
| Tue, 15 Apr 2008 18:49:13 +0200 |
Sign.hide_const;
|
file | diff | annotate |
| Tue, 08 Apr 2008 18:30:40 +0200 |
Generic conversion and tactic "atomize_elim" to convert elimination rules
|
file | diff | annotate |
| Fri, 04 Apr 2008 13:40:21 +0200 |
postprocessing of equality
|
file | diff | annotate |