equal
deleted
inserted
replaced
3 (* ------------------------------------------------------------------------- *) |
3 (* ------------------------------------------------------------------------- *) |
4 (* expand fixed point properties of lmap *) |
4 (* expand fixed point properties of lmap *) |
5 (* ------------------------------------------------------------------------- *) |
5 (* ------------------------------------------------------------------------- *) |
6 |
6 |
7 bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def |
7 bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def |
8 "lmap = (LAM f s.case s of dnil => dnil | x ## l => f`x ## lmap`f`l )"); |
8 "lmap = (LAM f s. case s of dnil => dnil | x ## l => f`x ## lmap`f`l )"); |
9 |
9 |
10 (* ------------------------------------------------------------------------- *) |
10 (* ------------------------------------------------------------------------- *) |
11 (* recursive properties of lmap *) |
11 (* recursive properties of lmap *) |
12 (* ------------------------------------------------------------------------- *) |
12 (* ------------------------------------------------------------------------- *) |
13 |
13 |