Fri, 04 Nov 2011 17:19:33 +0100 |
wenzelm |
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 23:41:16 +0200 |
wenzelm |
tuned Named_Thms: proper binding;
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 21:52:57 +0200 |
wenzelm |
more standard attribute setup;
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 21:02:10 +0200 |
wenzelm |
localized quotient data;
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 20:26:38 +0200 |
wenzelm |
simplified/standardized signatures;
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 19:41:08 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 13:52:31 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying qconsts_lookup function for data access; removing odd NotFound exception
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 13:50:55 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
|
file |
diff |
annotate
|
Thu, 27 Oct 2011 13:50:54 +0200 |
bulwahn |
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Sat, 08 Jan 2011 17:14:48 +0100 |
wenzelm |
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 21:51:28 +0100 |
wenzelm |
more standard package setup;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 21:26:49 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 15:55:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 15:35:00 +0100 |
wenzelm |
more precise parentheses and indentation;
|
file |
diff |
annotate
|
Fri, 07 Jan 2011 14:58:15 +0100 |
wenzelm |
comments;
|
file |
diff |
annotate
|
Thu, 28 Oct 2010 22:11:06 +0200 |
wenzelm |
handle Type.TYPE_MATCH, not arbitrary exceptions via MATCH_TYPE variable;
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 21:04:22 +0200 |
wenzelm |
more uniform descriptions, which end up in the collective output of 'print_attributes' for example;
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 16:34:10 +0200 |
wenzelm |
simplification/standardization of some theory data;
|
file |
diff |
annotate
|
Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
Fri, 23 Jul 2010 18:42:35 +0200 |
wenzelm |
observe standard conventions for doc-strings;
|
file |
diff |
annotate
|
Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Sun, 14 Mar 2010 14:31:24 +0100 |
wenzelm |
observe standard header format;
|
file |
diff |
annotate
|
Tue, 23 Feb 2010 14:11:46 +0100 |
Cezary Kaliszyk |
export prs_rules and rsp_rules attributes
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 10:28:00 +0100 |
Cezary Kaliszyk |
rename print_maps to print_quotmaps
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 22:06:52 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 13:54:19 +0100 |
Cezary Kaliszyk |
Initial version of HOL quotient package.
|
file |
diff |
annotate
|