| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 17:52:51 +0200 |
berghofe |
Deleted code for axiomatic introduction of datatypes. Instead, the package
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:55:49 +0100 |
wenzelm |
purely functional setup of claset/simpset/clasimpset;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:44 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2008 08:52:52 +0100 |
haftmann |
added combinator for interpretation of construction of datatype
|
file |
diff |
annotate
|
| Fri, 22 Feb 2008 12:01:54 +0100 |
haftmann |
added first version of datatype antiquotation
|
file |
diff |
annotate
|
| Mon, 18 Feb 2008 22:56:53 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 19:18:14 +0100 |
berghofe |
Eliminated DatatypeAux.dest_TFree to avoid clashes
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:31:52 +0100 |
berghofe |
- Removed redundant head_len field in datatype_info
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:15:59 +0100 |
haftmann |
interface and distinct simproc tuned
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 16:44:20 +0100 |
wenzelm |
ObjectLogic.typedecl;
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:30 +0100 |
haftmann |
separated typedecl module, providing typedecl command with interpretation
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 16:05:23 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
file |
diff |
annotate
|
| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
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
|
| Sun, 30 Sep 2007 16:20:31 +0200 |
wenzelm |
Sign.add_consts_authentic: tags (Markup.property list);
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 15:34:35 +0200 |
wenzelm |
simplified interpretation setup;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:36:15 +0200 |
haftmann |
distinction between regular and default code theorems
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:44 +0200 |
haftmann |
clarified class interfaces and internals
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:20 +0200 |
haftmann |
overloaded definitions accompanied by explicit constants
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:10:13 +0200 |
nipkow |
Final mods for list comprehension
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:30 +0200 |
haftmann |
using canonical instantiation interface
|
file |
diff |
annotate
|
| Fri, 10 Aug 2007 17:04:24 +0200 |
haftmann |
ClassPackage renamed to Class
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 21:19:20 +0200 |
wenzelm |
replaced dtK ref by datatype_distinctness_limit configuration option;
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:17 +0200 |
haftmann |
abstract size function in hologic.ML
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 15:11:07 +0200 |
berghofe |
- Moved parse / print translations for case to datatype_case.ML
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:38 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:37 +0100 |
haftmann |
switched exception from arbitrary to undefined
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:08 +0100 |
wenzelm |
moved parts of OuterParse to SpecParse;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 21:39:26 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 16:46:14 +0100 |
paulson |
Removal of theorem tagging, which the ATP linkup no longer requires,
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:30:38 +0100 |
wenzelm |
thm/prf: separate official name vs. additional tags;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:19 +0100 |
haftmann |
no explicit check for theory Nat
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:28 +0100 |
haftmann |
added instance for class size
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 00:15:38 +0100 |
wenzelm |
incorporated IsarThy into IsarCmd;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 21:45:14 +0100 |
wenzelm |
case_tr': proper handling of authentic consts;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 19:48:36 +0100 |
haftmann |
renamed DatatypeHooks.invoke to all
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:29 +0100 |
wenzelm |
removed theory NatArith (now part of Nat);
|
file |
diff |
annotate
|
| Sun, 05 Nov 2006 21:44:42 +0100 |
wenzelm |
case_tr: do not intern already internal consts;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2006 14:58:16 +0100 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:21 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:23 +0200 |
wenzelm |
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:35 +0200 |
haftmann |
handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:22:05 +0200 |
haftmann |
code generation 2 adjustments
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 17:30:36 +0200 |
wenzelm |
RuleInsts.bires_inst_tac;
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:37:41 +0200 |
wenzelm |
Variable.import(T): result includes fixed types/terms;
|
file |
diff |
annotate
|
| Fri, 21 Jul 2006 14:47:22 +0200 |
haftmann |
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
|
file |
diff |
annotate
|
| Fri, 21 Jul 2006 14:11:14 +0200 |
berghofe |
Some cases in "case ... of ..." expressions may now
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:42 +0200 |
wenzelm |
distinct simproc/simpset: proper context;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 20:21:30 +0200 |
wenzelm |
eliminated freeze/varify in favour of Variable.import/export/trade;
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:34 +0200 |
wenzelm |
ProjectRule now context dependent;
|
file |
diff |
annotate
|