Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Isar_Ref/HOL_Specific.thy
changeset 59845 fafb4d12c307
parent 59785 4e6ab5831cc0
child 59905 678c9e625782 
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 29 21:30:28 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Mar 29 21:47:16 2015 +0200
@@ -2338,7 +2338,7 @@
     ;
     @@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
     ;
-    @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
+    @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
     ;
     @@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
     ;
isabelle