# 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