# HG changeset patch
# User lcp
# Date 767957331 -7200
# Node ID 1718ce07a584b2a9a43064955d3107857b15461a
# Parent  d9ebca601847cc65a1e0bc8846c7ecf3cd300a29
removal of obsolete type-declaration syntax

diff -r d9ebca601847 -r 1718ce07a584 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Tue May 03 11:17:08 1994 +0200
+++ b/src/Cube/Cube.thy	Tue May 03 11:28:51 1994 +0200
@@ -9,7 +9,7 @@
 Cube = Pure +
 
 types
-  term, context, typing 0
+  term  context  typing
 
 arities
   term :: logic
diff -r d9ebca601847 -r 1718ce07a584 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue May 03 11:17:08 1994 +0200
+++ b/src/ZF/ZF.thy	Tue May 03 11:28:51 1994 +0200
@@ -9,7 +9,7 @@
 ZF = FOL +
 
 types
-  i, is 0
+  i  is
 
 arities
   i :: term