# HG changeset patch
# User berghofe
# Date 934985941 -7200
# Node ID 0a69baf2896109c0295f53c630994b9790965093
# Parent  853bdbe9973d004f4b5fa218cbd762878fd86327
Eliminated some infixes.

diff -r 853bdbe9973d -r 0a69baf28961 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Wed Aug 18 16:12:20 1999 +0200
+++ b/src/HOL/Induct/LList.ML	Wed Aug 18 16:19:01 1999 +0200
@@ -19,7 +19,7 @@
 qed "llist_mono";
 
 
-Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
+Goal "llist(A) = usum {Numb(0)} (uprod A (llist A))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
 by (fast_tac (claset() addSIs (map rew llist.intrs)
                        addEs [rew llist.elim]) 1)
@@ -120,7 +120,7 @@
 (**** llist equality as a gfp; the bisimulation principle ****)
 
 (*This theorem is actually used, unlike the many similar ones in ZF*)
-Goal "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
+Goal "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))";
 let val rew = rewrite_rule [NIL_def, CONS_def] in  
 by (fast_tac (claset() addSIs (map rew LListD.intrs)
                       addEs [rew LListD.elim]) 1)
diff -r 853bdbe9973d -r 0a69baf28961 src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Wed Aug 18 16:12:20 1999 +0200
+++ b/src/HOL/Induct/SList.ML	Wed Aug 18 16:19:01 1999 +0200
@@ -17,7 +17,7 @@
 
 val list_con_defs = [NIL_def, CONS_def];
 
-Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
+Goal "list(A) = usum {Numb(0)} (uprod A (list A))";
 let val rew = rewrite_rule list_con_defs in  
 by (fast_tac (claset() addSIs (equalityI :: map rew list.intrs)
                       addEs [rew list.elim]) 1)