equal
deleted
inserted
replaced
10 RegExp2NAe = NAe + RegExp + |
10 RegExp2NAe = NAe + RegExp + |
11 |
11 |
12 types 'a bitsNAe = ('a,bool list)nae |
12 types 'a bitsNAe = ('a,bool list)nae |
13 |
13 |
14 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65) |
14 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65) |
15 translations "x ## S" == "op # x `` S" |
15 translations "x ## S" == "Cons x `` S" |
16 |
16 |
17 constdefs |
17 constdefs |
18 atom :: 'a => 'a bitsNAe |
18 atom :: 'a => 'a bitsNAe |
19 "atom a == ([True], |
19 "atom a == ([True], |
20 %b s. if s=[True] & b=Some a then {[False]} else {}, |
20 %b s. if s=[True] & b=Some a then {[False]} else {}, |