src/HOL/Induct/LList.ML
changeset 5143 b94cd208f073
parent 5102 8c782c25a11e
child 5148 74919e8f221c
     1.1 --- a/src/HOL/Induct/LList.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  Addsplits [split_split, split_sum_case];
     1.5  
     1.6  (*This justifies using llist in other recursive type definitions*)
     1.7 -Goalw llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
     1.8 +Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
     1.9  by (rtac gfp_mono 1);
    1.10  by (REPEAT (ares_tac basic_monos 1));
    1.11  qed "llist_mono";
    1.12 @@ -190,7 +190,7 @@
    1.13      THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
    1.14   **)
    1.15  
    1.16 -Goalw [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
    1.17 +Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
    1.18  by (REPEAT (ares_tac basic_monos 1));
    1.19  qed "LListD_Fun_mono";
    1.20  
    1.21 @@ -335,7 +335,7 @@
    1.22  
    1.23  (*A typical use of co-induction to show membership in the gfp.
    1.24    The containing set is simply the singleton {Lconst(M)}. *)
    1.25 -Goal "!!M A. M:A ==> Lconst(M): llist(A)";
    1.26 +Goal "M:A ==> Lconst(M): llist(A)";
    1.27  by (rtac (singletonI RS llist_coinduct) 1);
    1.28  by Safe_tac;
    1.29  by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
    1.30 @@ -522,12 +522,12 @@
    1.31            Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
    1.32  
    1.33  
    1.34 -Goal "!!M. M: llist(A) ==> Lappend NIL M = M";
    1.35 +Goal "M: llist(A) ==> Lappend NIL M = M";
    1.36  by (etac LList_fun_equalityI 1);
    1.37  by (ALLGOALS Asm_simp_tac);
    1.38  qed "Lappend_NIL";
    1.39  
    1.40 -Goal "!!M. M: llist(A) ==> Lappend M NIL = M";
    1.41 +Goal "M: llist(A) ==> Lappend M NIL = M";
    1.42  by (etac LList_fun_equalityI 1);
    1.43  by (ALLGOALS Asm_simp_tac);
    1.44  qed "Lappend_NIL2";