| Fri, 12 Feb 2010 09:49:28 +0100 |
haftmann |
tuned comments
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
| Wed, 07 Oct 2009 12:06:04 +0200 |
haftmann |
do not use Locale.add_registration_eqs any longer
|
file |
diff |
annotate
|
| Thu, 01 Oct 2009 17:11:48 +0200 |
haftmann |
proper merge of interpretation equations
|
file |
diff |
annotate
|
| Sun, 27 Sep 2009 09:52:25 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Sat, 25 Jul 2009 18:44:55 +0200 |
haftmann |
improved handling of parameter import; tuned
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 16:49:05 +0200 |
haftmann |
dropped add_registration interface in locale
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 07:59:28 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 20:36:38 +0200 |
wenzelm |
clarified Thm.of_class/of_sort/class_triv;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 19:58:52 +0200 |
wenzelm |
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 21:26:18 +0200 |
wenzelm |
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:28:02 +0200 |
wenzelm |
renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 17:42:36 +0200 |
haftmann |
skip_proof where appropriate
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 08:16:09 +0200 |
haftmann |
skip_proof not operative here
|
file |
diff |
annotate
|
| Sun, 14 Jun 2009 17:20:19 +0200 |
haftmann |
using skip_proof where appropriate
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 20:25:23 +0100 |
wenzelm |
simplified Locale.activate operations, using generic context;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 16:00:54 +0100 |
wenzelm |
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 13:28:55 +0100 |
wenzelm |
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 22:16:50 +0100 |
wenzelm |
more uniform handling of binding in targets and derived elements;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 11:32:31 +0100 |
wenzelm |
Binding.str_of: removed verbose feature, include qualifier in output;
|
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
|
| Tue, 03 Mar 2009 18:32:01 +0100 |
wenzelm |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 14:07:43 +0100 |
wenzelm |
Thm.binding;
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 09:05:20 +0100 |
haftmann |
more robust failure in error situations
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 21:26:21 +0100 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|