src/HOL/Induct/LList.ML
changeset 7256 0a69baf28961
parent 5996 6b6e0ede3517
child 7825 1be9b63e7d93
     1.1 --- a/src/HOL/Induct/LList.ML	Wed Aug 18 16:12:20 1999 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Aug 18 16:19:01 1999 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  qed "llist_mono";
     1.5  
     1.6  
     1.7 -Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
     1.8 +Goal "llist(A) = usum {Numb(0)} (uprod A (llist A))";
     1.9  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    1.10  by (fast_tac (claset() addSIs (map rew llist.intrs)
    1.11                         addEs [rew llist.elim]) 1)
    1.12 @@ -120,7 +120,7 @@
    1.13  (**** llist equality as a gfp; the bisimulation principle ****)
    1.14  
    1.15  (*This theorem is actually used, unlike the many similar ones in ZF*)
    1.16 -Goal "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
    1.17 +Goal "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))";
    1.18  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    1.19  by (fast_tac (claset() addSIs (map rew LListD.intrs)
    1.20                        addEs [rew LListD.elim]) 1)