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/ZF/AC/Transrec2.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c 
--- a/src/ZF/AC/Transrec2.thy	Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/AC/Transrec2.thy	Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/AC/Transrec2.thy
+(*  Title:      ZF/AC/Transrec2.thy
     ID:         $Id$
-    Author: 	Krzysztof Grabczewski
+    Author:     Krzysztof Grabczewski
 
 Transfinite recursion introduced to handle definitions based on the three
 cases of ordinals.
@@ -14,10 +14,10 @@
 
 defs
 
-  transrec2_def  "transrec2(alpha, a, b) ==   			
-		         transrec(alpha, %i r. if(i=0,   	
-		                  a, if(EX j. i=succ(j),   	
-		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
-		                  UN j<i. r`j)))"
+  transrec2_def  "transrec2(alpha, a, b) ==                     
+                         transrec(alpha, %i r. if(i=0,          
+                                  a, if(EX j. i=succ(j),        
+                                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
+                                  UN j<i. r`j)))"
 
 end
isabelle