Eliminated some infixes.
authorberghofe
Wed Aug 18 16:19:01 1999 +0200 (1999-08-18)
changeset 72560a69baf28961
parent 7255 853bdbe9973d
child 7257 745cfc8871e2
Eliminated some infixes.
src/HOL/Induct/LList.ML
src/HOL/Induct/SList.ML
     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)
     2.1 --- a/src/HOL/Induct/SList.ML	Wed Aug 18 16:12:20 1999 +0200
     2.2 +++ b/src/HOL/Induct/SList.ML	Wed Aug 18 16:19:01 1999 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5  val list_con_defs = [NIL_def, CONS_def];
     2.6  
     2.7 -Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
     2.8 +Goal "list(A) = usum {Numb(0)} (uprod A (list A))";
     2.9  let val rew = rewrite_rule list_con_defs in  
    2.10  by (fast_tac (claset() addSIs (equalityI :: map rew list.intrs)
    2.11                        addEs [rew list.elim]) 1)