# HG changeset patch
# User berghofe
# Date 908985422 -7200
# Node ID 458a67fd54611438255fd16f33e6b7af5f43c613
# Parent  ace664b0c978a531ea136f66589a5431d12c462b
Changed interface of inductive.

diff -r ace664b0c978 -r 458a67fd5461 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed Oct 21 17:55:18 1998 +0200
+++ b/src/HOL/UNITY/WFair.thy	Wed Oct 21 17:57:02 1998 +0200
@@ -36,7 +36,7 @@
     *)
     Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
 
-  monos "[Pow_mono]"
+  monos Pow_mono