--- a/src/HOL/Induct/Acc.thy Thu Aug 06 12:46:18 1998 +0200
+++ b/src/HOL/Induct/Acc.thy Thu Aug 06 12:46:38 1998 +0200
@@ -23,4 +23,7 @@
pred "pred a r: Pow(acc(r)) ==> a: acc(r)"
monos "[Pow_mono]"
+syntax termi :: "('a * 'a)set => 'a set"
+translations "termi r" == "acc(r^-1)"
+
end