| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:27:05 +0200 |
ballarin |
Clearer separation of interpretation frontend and backend.
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:30 +0200 |
wenzelm |
Sign.declare_const: Name.binding;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 11:44:48 +0200 |
wenzelm |
Name.qualified;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 17:54:31 +0200 |
ballarin |
Consistent naming of theorems in interpretation.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:00:28 +0200 |
wenzelm |
get rid of tabs;
|
file |
diff |
annotate
|
| Tue, 26 Aug 2008 16:04:22 +0200 |
ballarin |
Reorganisation of registration code.
|
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
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 17:41:37 +0200 |
ballarin |
Removed import and lparams from locale record.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 07:33:59 +0200 |
haftmann |
facts_of
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:44 +0200 |
haftmann |
tuned; explicit export of element accessors
|
file |
diff |
annotate
|
| Sat, 26 Jul 2008 09:00:26 +0200 |
haftmann |
tuned function name
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:41 +0200 |
wenzelm |
Syntax.string_of_typ: proper context;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 17:54:56 +0200 |
ballarin |
Changed naming scheme for theorems generated by interpretations.
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:48 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:49 +0100 |
wenzelm |
renamed former get_thms(_silent) to get_fact(_silent);
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:36:04 +0100 |
wenzelm |
closeup: recover original order of free variables!
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 22:58:11 +0100 |
wenzelm |
closeup: minor tuning of term traversal;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 17:57:52 +0100 |
haftmann |
explicit closing of derived witnesses
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:07 +0100 |
haftmann |
memorizing and exporting destruction rules
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 22:19:43 +0100 |
wenzelm |
avoid "import" as identifier, which is a keyword in Alice;
|
file |
diff |
annotate
|