--- a/src/HOL/Calculation.thy Thu Feb 10 13:34:52 2000 +0100 +++ b/src/HOL/Calculation.thy Thu Feb 10 13:36:23 2000 +0100 @@ -52,5 +52,7 @@ theorems [trans] = trans (* = = = *) +theorems [elim??] = sym + end;