src/ZF/Coind/Map.thy

--- a/src/ZF/Coind/Map.thy	Tue Mar 07 13:29:36 1995 +0100
+++ b/src/ZF/Coind/Map.thy	Tue Mar 07 13:32:22 1995 +0100
@@ -9,7 +9,7 @@
 consts
   TMap :: "[i,i] => i"
   PMap :: "[i,i] => i"
-rules
+defs
   TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
   PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
 
@@ -19,7 +19,7 @@
   map_emp :: "i"
   map_owr :: "[i,i,i]=>i"
   map_app :: "[i,i]=>i"
-rules
+defs
   map_emp_def "map_emp == 0"
   map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
   map_app_def "map_app(m,a) == m``{a}"