Tue, 02 Jun 2009 10:02:52 +0200 |
berghofe |
Fixed broken code dealing with alternative names.
|
file |
diff |
annotate
|
Sun, 24 May 2009 15:02:22 +0200 |
haftmann |
refined construction_interpretation
|
file |
diff |
annotate
|
Wed, 20 May 2009 10:37:37 +0200 |
haftmann |
parse translations for cases are conservative wrt. overloaded constructors
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
avoid inspecting pretty output
|
file |
diff |
annotate
|
Mon, 09 Mar 2009 17:54:27 +0100 |
wenzelm |
adapted to simplified ThyOutput.antiquotation interface;
|
file |
diff |
annotate
|
Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
Sat, 07 Mar 2009 22:17:25 +0100 |
wenzelm |
more uniform handling of binding in packages;
|
file |
diff |
annotate
|
Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 13:41:59 +0100 |
haftmann |
datatype antiquotation does not assume LaTeX as output any longer
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Mon, 02 Mar 2009 16:58:39 +0100 |
haftmann |
better markup
|
file |
diff |
annotate
|
Fri, 20 Feb 2009 18:33:28 +0100 |
haftmann |
datatype antiquotation: always bracket types with spaces in between
|
file |
diff |
annotate
|
Fri, 13 Feb 2009 16:47:08 +0100 |
berghofe |
Tuned datatype antiquotation.
|
file |
diff |
annotate
|
Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
Wed, 31 Dec 2008 18:53:16 +0100 |
wenzelm |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file |
diff |
annotate
|
Wed, 10 Dec 2008 22:55:15 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Tue, 28 Oct 2008 16:58:59 +0100 |
haftmann |
cleanup code default attribute
|
file |
diff |
annotate
|
Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
Fri, 20 Jun 2008 21:00:22 +0200 |
haftmann |
DatatypeProp.make_distincts: only one half of each symmetric pair is constructed
|
file |
diff |
annotate
|
Thu, 19 Jun 2008 20:48:01 +0200 |
wenzelm |
export read_typ/cert_typ -- version with regular context operations;
|
file |
diff |
annotate
|
Wed, 18 Jun 2008 18:55:10 +0200 |
wenzelm |
eliminated old Sign.read_term/Thm.read_cterm etc.;
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 19:15:23 +0200 |
wenzelm |
moved case_tac/induct_tac to induct_tacs.ML -- no longer hardwired into datatype package;
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
Mon, 09 Jun 2008 17:07:11 +0200 |
wenzelm |
signature cleanup -- no pervasives anymore;
|
file |
diff |
annotate
|
Wed, 28 May 2008 14:48:50 +0200 |
haftmann |
moved distinctness_limit to datatype_rep_proofs.ML
|
file |
diff |
annotate
|
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
|