equal
deleted
inserted
replaced
36 Leadsto (infixr "\<leadsto>" 22) |
36 Leadsto (infixr "\<leadsto>" 22) |
37 |
37 |
38 defs |
38 defs |
39 |
39 |
40 unlift_def: |
40 unlift_def: |
41 "unlift x == (case x of |
41 "unlift x == (case x of Def y => y)" |
42 UU => arbitrary |
|
43 | Def y => y)" |
|
44 |
42 |
45 (* this means that for nil and UU the effect is unpredictable *) |
43 (* this means that for nil and UU the effect is unpredictable *) |
46 Init_def: |
44 Init_def: |
47 "Init P s == (P (unlift (HD$s)))" |
45 "Init P s == (P (unlift (HD$s)))" |
48 |
46 |