equal
deleted
inserted
replaced
45 by (rtac lfp_mono 1); |
45 by (rtac lfp_mono 1); |
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
46 by (REPEAT (rtac ListN.bnd_mono 1)); |
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
47 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); |
48 val listn_mono = result(); |
48 val listn_mono = result(); |
49 |
49 |
|
50 val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)" |
|
51 and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,xs)> : listn(A)"; |
|
52 |