src/HOL/Induct/LList.ML
changeset 7825 1be9b63e7d93
parent 7256 0a69baf28961
child 8114 09a7a180cc99
     1.1 --- a/src/HOL/Induct/LList.ML	Mon Oct 11 10:51:24 1999 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Mon Oct 11 10:52:51 1999 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  
     1.5  (*A typical use of co-induction to show membership in the gfp. 
     1.6    Bisimulation is  range(%x. LList_corec x f) *)
     1.7 -Goal "LList_corec a f : llist({u. True})";
     1.8 +Goal "LList_corec a f : llist UNIV";
     1.9  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.10  by (rtac rangeI 1);
    1.11  by Safe_tac;
    1.12 @@ -247,14 +247,14 @@
    1.13  \ ==> h1=h2";
    1.14  by (rtac ext 1);
    1.15  (*next step avoids an unknown (and flexflex pair) in simplification*)
    1.16 -by (res_inst_tac [("A", "{u. True}"),
    1.17 +by (res_inst_tac [("A", "UNIV"),
    1.18                    ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
    1.19  by (rtac rangeI 1);
    1.20  by Safe_tac;
    1.21  by (stac prem1 1);
    1.22  by (stac prem2 1);
    1.23  by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
    1.24 -				  CollectI RS LListD_Fun_CONS_I]) 1);
    1.25 +				  UNIV_I RS LListD_Fun_CONS_I]) 1);
    1.26  qed "LList_corec_unique";
    1.27  
    1.28  val [prem] =