--- a/src/HOL/indrule.thy Mon Nov 03 12:05:42 1997 +0100 +++ b/src/HOL/indrule.thy Mon Nov 03 12:07:13 1997 +0100 @@ -1,1 +1,2 @@ -indrule = "intr_elim" + +indrule = intr_elim