| 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
|
| Mon, 08 Oct 2007 08:04:28 +0200 |
haftmann |
added first version of user-space type system for class target
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:54:44 +0200 |
haftmann |
certificates for code generator case expressions
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 19:42:03 +0200 |
haftmann |
clarified declarations in class ord
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
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 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:05:34 +0200 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 17:56:03 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 18:24:34 +0200 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
| Thu, 16 Aug 2007 11:45:06 +0200 |
haftmann |
fixed codegen setup
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:39 +0200 |
haftmann |
updated code generator setup
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:34 +0200 |
haftmann |
new structure for code generator modules
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:40:34 +0200 |
haftmann |
new nbe implementation
|
file |
diff |
annotate
|
| Sun, 29 Jul 2007 14:29:49 +0200 |
wenzelm |
simplified ResAtpset via NamedThmsFun;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:45 +0200 |
haftmann |
using class target
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Wed, 04 Jul 2007 16:49:34 +0200 |
wenzelm |
replaced HOLogic.Trueprop_conv by ObjectLogic.judgment_conv;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 22:27:05 +0200 |
wenzelm |
use hologic.ML in basic HOL context;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2007 19:09:32 +0200 |
haftmann |
simplified keyword setup
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:22 +0200 |
chaieb |
added Theorem all_not_ex
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|