| 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 |
| Wed, 02 Apr 2008 15:58:32 +0200 |
explicit class "eq" for operational equality
|
file | diff | annotate |
| Sat, 29 Mar 2008 22:55:49 +0100 |
purely functional setup of claset/simpset/clasimpset;
|
file | diff | annotate |
| Wed, 26 Mar 2008 22:40:01 +0100 |
pass imp_elim, swap to classical prover;
|
file | diff | annotate |
| Fri, 25 Jan 2008 14:54:44 +0100 |
dropped superfluous code theorems
|
file | diff | annotate |
| Wed, 02 Jan 2008 15:14:02 +0100 |
splitted class uminus from class minus
|
file | diff | annotate |
| Sat, 22 Dec 2007 14:10:22 +0100 |
use random_word.ML earlier;
|
file | diff | annotate |
| Wed, 05 Dec 2007 14:15:45 +0100 |
simplified infrastructure for code generator operational equality
|
file | diff | annotate |
| Wed, 28 Nov 2007 16:44:18 +0100 |
replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);
|
file | diff | annotate |
| Fri, 23 Nov 2007 21:09:33 +0100 |
interpretation of typedecls: instantiation to class type
|
file | diff | annotate |
| Sun, 11 Nov 2007 14:00:05 +0100 |
tuned specifications of 'notation';
|
file | diff | annotate |
| Mon, 05 Nov 2007 22:50:00 +0100 |
move itself into HOL types
|
file | diff | annotate |
| Tue, 16 Oct 2007 23:12:45 +0200 |
global class syntax
|
file | diff | annotate |
| Mon, 08 Oct 2007 08:04:28 +0200 |
added first version of user-space type system for class target
|
file | diff | annotate |
| Thu, 04 Oct 2007 19:54:44 +0200 |
certificates for code generator case expressions
|
file | diff | annotate |
| Thu, 04 Oct 2007 19:42:03 +0200 |
clarified declarations in class ord
|
file | diff | annotate |
| Thu, 04 Oct 2007 14:42:47 +0200 |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file | diff | annotate |
| Sat, 29 Sep 2007 08:58:51 +0200 |
proper syntax during class specification
|
file | diff | annotate |
| Tue, 18 Sep 2007 18:05:34 +0200 |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file | diff | annotate |