| Fri, 19 Feb 2010 20:41:34 +0100 |
wenzelm |
Thm.def_binding;
|
changeset |
files
|
| Fri, 19 Feb 2010 20:39:48 +0100 |
wenzelm |
moved ancient Drule.get_def to OldGoals.get_def;
|
changeset |
files
|
| Fri, 19 Feb 2010 17:37:33 +0100 |
Cezary Kaliszyk |
quote the constant and theorem name with @{text}
|
changeset |
files
|
| Fri, 19 Feb 2010 17:03:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 19 Feb 2010 16:49:23 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 19 Feb 2010 16:45:21 +0100 |
wenzelm |
local Simplifier.context;
|
changeset |
files
|
| Fri, 19 Feb 2010 16:11:45 +0100 |
wenzelm |
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
|
changeset |
files
|
| Fri, 19 Feb 2010 11:56:11 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Fri, 19 Feb 2010 11:49:44 +0100 |
wenzelm |
Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
|
changeset |
files
|
| Fri, 19 Feb 2010 16:42:37 +0100 |
haftmann |
merged
|
changeset |
files
|
| Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
context theorem is optional
|
changeset |
files
|
| Fri, 19 Feb 2010 11:06:22 +0100 |
haftmann |
added dest_comb
|
changeset |
files
|