# HG changeset patch
# User krauss
# Date 1288088341 -7200
# Node ID 751121d5ca3550155cee99f3fc61bb14a182e72c
# Parent  11ea439d947f23ca85f9dd30b47a8a8d6a7a667f
remove outdated "(otherwise)" syntax from manual

diff -r 11ea439d947f -r 751121d5ca35 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Oct 26 12:19:01 2010 +0200
@@ -401,12 +401,10 @@
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
+    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
+    ;
     equations: (thmdecl? prop + '|')
     ;
-    ('fun' | 'function') target? functionopts? fixes 'where' clauses
-    ;
-    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
-    ;
     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;
     'termination' ( term )?
diff -r 11ea439d947f -r 751121d5ca35 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Oct 26 12:19:01 2010 +0200
@@ -411,12 +411,10 @@
   \begin{rail}
     'primrec' target? fixes 'where' equations
     ;
+    ('fun' | 'function') target? functionopts? fixes \\ 'where' equations
+    ;
     equations: (thmdecl? prop + '|')
     ;
-    ('fun' | 'function') target? functionopts? fixes 'where' clauses
-    ;
-    clauses: (thmdecl? prop ('(' 'otherwise' ')')? + '|')
-    ;
     functionopts: '(' (('sequential' | 'domintros' | 'tailrec' | 'default' term) + ',') ')'
     ;
     'termination' ( term )?