equal
deleted
inserted
replaced
8 imports TLS |
8 imports TLS |
9 begin |
9 begin |
10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 types |
13 type_synonym |
14 ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" |
14 ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp" |
15 |
15 |
16 definition |
16 definition |
17 validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where |
17 validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where |
18 "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)" |
18 "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)" |