| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 21:59:18 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 20:14:45 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 13:44:01 +0100 |
wenzelm |
more uniform check_const/read_const;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:43:29 +0100 |
wenzelm |
more rigid type_name demands, based on educated guesses about the tools involved here;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 12:10:19 +0100 |
wenzelm |
tuned signature -- more uniform check_type_name/read_type_name;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 10:56:56 +0200 |
wenzelm |
merged, resolving trivial conflict;
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:20:09 +0100 |
kuncar |
store the relational theorem for every relator
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 14:18:43 +0100 |
kuncar |
store the quotient theorem for every quotient
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 20:32:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 21:59:19 +0100 |
wenzelm |
afford strict Args.type_name (cf. 29e88714ffe4);
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Fri, 09 Dec 2011 18:07:04 +0100 |
kuncar |
Quotient_Info stores only relation maps
|
file |
diff |
annotate
|
| Thu, 17 Nov 2011 14:35:32 +0100 |
bulwahn |
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
|
file |
diff |
annotate
|
| Sat, 05 Nov 2011 12:01:21 +0000 |
Christian Urban |
more use of global operations (see 98ec8b51af9c)
|
file |
diff |
annotate
|
| 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
|