Sat, 20 Jan 2007 14:09:12 +0100 |
wenzelm |
tuned ML setup;
|
file |
diff |
annotate
|
Wed, 06 Dec 2006 01:12:42 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
Mon, 27 Nov 2006 13:42:39 +0100 |
haftmann |
moved order arities for fun and bool to Fun/Orderings
|
file |
diff |
annotate
|
Sun, 26 Nov 2006 18:07:16 +0100 |
wenzelm |
updated (binder) syntax/notation;
|
file |
diff |
annotate
|
Thu, 23 Nov 2006 22:38:28 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Thu, 23 Nov 2006 20:34:21 +0100 |
wenzelm |
prefer antiquotations over LaTeX macros;
|
file |
diff |
annotate
|
Thu, 23 Nov 2006 13:32:19 +0100 |
webertj |
typo in comment fixed
|
file |
diff |
annotate
|
Sat, 18 Nov 2006 00:20:17 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Wed, 08 Nov 2006 19:48:35 +0100 |
haftmann |
moved lemma eq_neq_eq_imp_neq to HOL
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 14:29:57 +0100 |
wenzelm |
tuned hypsubst setup;
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
Sun, 05 Nov 2006 21:44:32 +0100 |
wenzelm |
Sign.const_syntax_name;
|
file |
diff |
annotate
|
Fri, 03 Nov 2006 14:22:37 +0100 |
haftmann |
simplified reasoning tools setup
|
file |
diff |
annotate
|
Tue, 31 Oct 2006 09:28:55 +0100 |
haftmann |
added Equals_conv
|
file |
diff |
annotate
|
Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
Fri, 13 Oct 2006 12:32:44 +0200 |
haftmann |
lifted claset setup from ML to Isar level
|
file |
diff |
annotate
|
Wed, 11 Oct 2006 14:51:24 +0200 |
haftmann |
cleaned up HOL bootstrap
|
file |
diff |
annotate
|
Tue, 10 Oct 2006 10:35:24 +0200 |
haftmann |
cleanup basic HOL bootstrap
|
file |
diff |
annotate
|
Mon, 02 Oct 2006 23:00:49 +0200 |
haftmann |
improved serialization for arbitrary
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 23:42:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 27 Sep 2006 21:49:34 +0200 |
wenzelm |
proper const_syntax for uminus, abs;
|
file |
diff |
annotate
|
Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
Mon, 25 Sep 2006 17:04:14 +0200 |
haftmann |
added 'undefined' serializer
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:21:44 +0200 |
haftmann |
introduced syntactic classes; moved some setup to Pure/codegen, Pure/nbe or OperationalEquality.thy
|
file |
diff |
annotate
|
Fri, 01 Sep 2006 08:36:51 +0200 |
haftmann |
final syntax for some Isar code generator keywords
|
file |
diff |
annotate
|
Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
Thu, 27 Jul 2006 13:43:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Fri, 21 Jul 2006 11:34:01 +0200 |
berghofe |
- Added new "undefined" constant
|
file |
diff |
annotate
|
Fri, 07 Jul 2006 09:31:57 +0200 |
nipkow |
made evaluation_conv and normalization_conv visible.
|
file |
diff |
annotate
|
Wed, 05 Jul 2006 16:24:28 +0200 |
paulson |
removed the "tagging" feature
|
file |
diff |
annotate
|
Fri, 30 Jun 2006 18:26:22 +0200 |
nipkow |
normalization uses refl now
|
file |
diff |
annotate
|
Thu, 29 Jun 2006 13:52:28 +0200 |
nipkow |
new method "normalization"
|
file |
diff |
annotate
|
Wed, 14 Jun 2006 12:14:42 +0200 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
Tue, 06 Jun 2006 20:42:25 +0200 |
wenzelm |
quoted "if";
|
file |
diff |
annotate
|
Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|
Tue, 09 May 2006 14:18:40 +0200 |
haftmann |
introduced characters for code generator; some improved code lemmas for some list functions
|
file |
diff |
annotate
|
Tue, 09 May 2006 10:09:17 +0200 |
haftmann |
different object logic setup for CodegenTheorems
|
file |
diff |
annotate
|
Tue, 02 May 2006 20:42:32 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
Thu, 06 Apr 2006 16:11:30 +0200 |
haftmann |
adapted for definitional code generation
|
file |
diff |
annotate
|
Fri, 10 Mar 2006 15:33:48 +0100 |
haftmann |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
file |
diff |
annotate
|
Thu, 02 Mar 2006 18:49:13 +0100 |
paulson |
moved the "use" directive
|
file |
diff |
annotate
|
Wed, 01 Mar 2006 06:08:12 +0100 |
mengj |
Added setup for "atpset" (a rule set for ATPs).
|
file |
diff |
annotate
|
Sat, 25 Feb 2006 15:19:47 +0100 |
haftmann |
improved codegen bootstrap
|
file |
diff |
annotate
|
Wed, 22 Feb 2006 22:18:32 +0100 |
wenzelm |
simplified Pure conjunction;
|
file |
diff |
annotate
|
Tue, 14 Feb 2006 17:07:48 +0100 |
haftmann |
added theory of executable rational numbers
|
file |
diff |
annotate
|
Wed, 01 Feb 2006 19:19:32 +0100 |
berghofe |
Added "evaluation" method and oracle.
|
file |
diff |
annotate
|
Tue, 31 Jan 2006 16:26:18 +0100 |
haftmann |
added serialization for arbitrary
|
file |
diff |
annotate
|
Sun, 29 Jan 2006 19:23:38 +0100 |
wenzelm |
declare 'defn' rules;
|
file |
diff |
annotate
|
Mon, 23 Jan 2006 14:07:52 +0100 |
haftmann |
removed problematic keyword 'atom'
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Tue, 17 Jan 2006 16:36:57 +0100 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|
Mon, 16 Jan 2006 21:55:14 +0100 |
wenzelm |
declare the1_equality [elim?];
|
file |
diff |
annotate
|
Sun, 15 Jan 2006 19:58:51 +0100 |
wenzelm |
prefer ex1I over ex_ex1I in single-step reasoning;
|
file |
diff |
annotate
|
Fri, 06 Jan 2006 18:18:13 +0100 |
wenzelm |
simplified EqSubst setup;
|
file |
diff |
annotate
|
Fri, 06 Jan 2006 15:18:20 +0100 |
wenzelm |
tuned EqSubst setup;
|
file |
diff |
annotate
|
Sat, 31 Dec 2005 21:49:39 +0100 |
wenzelm |
removed obsolete cla_dist_concl;
|
file |
diff |
annotate
|
Fri, 30 Dec 2005 16:56:56 +0100 |
wenzelm |
provide cla_dist_concl;
|
file |
diff |
annotate
|
Fri, 23 Dec 2005 18:36:26 +0100 |
wenzelm |
removed obsolete induct_atomize_old;
|
file |
diff |
annotate
|
Thu, 22 Dec 2005 00:28:36 +0100 |
wenzelm |
structure ProjectRule;
|
file |
diff |
annotate
|