--- a/src/ZF/UNITY/Increasing.thy Sun Oct 07 13:57:05 2007 +0200
+++ b/src/ZF/UNITY/Increasing.thy Sun Oct 07 15:49:25 2007 +0200
@@ -23,11 +23,9 @@
{F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
(\<forall>x \<in> state. f(x):A)}"
-syntax
- IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60)
-
-translations
- "IncWrt(f,r,A)" => "Increasing[A](r,f)"
+abbreviation (input)
+ IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) where
+ "f IncreasingWrt r/A == Increasing[A](r,f)"
(** increasing **)