# HG changeset patch
# User wenzelm
# Date 950186183 -3600
# Node ID 38f453607c61d4dc02f2d1ccc3688dbbacc6e448
# Parent  8283e416b680a1310a8da44b6fad5691707df26f
theorems [elim??] = sym;

diff -r 8283e416b680 -r 38f453607c61 src/HOL/Calculation.thy
--- 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;