src/ZF/list.ML
changeset 30 d49df4181f0d
parent 14 1c0926788772
child 55 331d93292ee0
equal deleted inserted replaced
29:4ec9b266ccd1 30:d49df4181f0d
    65 val list_case_type = result();
    65 val list_case_type = result();
    66 
    66 
    67 
    67 
    68 (** For recursion **)
    68 (** For recursion **)
    69 
    69 
    70 goalw List.thy List.con_defs "rank(a) : rank(Cons(a,l))";
    70 goalw List.thy List.con_defs "rank(a) < rank(Cons(a,l))";
    71 by (simp_tac rank_ss 1);
    71 by (simp_tac rank_ss 1);
    72 val rank_Cons1 = result();
    72 val rank_Cons1 = result();
    73 
    73 
    74 goalw List.thy List.con_defs "rank(l) : rank(Cons(a,l))";
    74 goalw List.thy List.con_defs "rank(l) < rank(Cons(a,l))";
    75 by (simp_tac rank_ss 1);
    75 by (simp_tac rank_ss 1);
    76 val rank_Cons2 = result();
    76 val rank_Cons2 = result();
    77 
    77