Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned comments;
authorwenzelm
Tue, 14 Mar 2000 11:33:30 +0100
changeset 8451 614f18139d47
parent 8450 dc44d6533f0f
child 8452 59d66fe9bbb9
tuned comments;
src/HOL/Tools/induct_method.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/induct_method.ML	Tue Mar 14 11:33:14 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Tue Mar 14 11:33:30 2000 +0100
@@ -185,7 +185,7 @@
         cases         - classical case split
         cases t       - datatype exhaustion
   <x:A> cases ...     - set elimination
-  ...   cases ... r   - explicit rule
+  ...   cases ... R   - explicit rule
 *)
 
 local
@@ -248,7 +248,7 @@
         induct         - mathematical induction
         induct x       - datatype induction
   <x:A> induct ...     - set induction
-  ...   induct ... r   - explicit rule
+  ...   induct ... R   - explicit rule
 *)
 
 local
isabelle