| changeset 7224 | e41e64476f9b |
| parent 5323 | 028e00595280 |
| child 8732 | aef229ca5e77 |
--- a/src/HOL/Lex/RegExp2NA.thy Mon Aug 16 22:04:07 1999 +0200 +++ b/src/HOL/Lex/RegExp2NA.thy Mon Aug 16 22:07:12 1999 +0200 @@ -12,7 +12,7 @@ types 'a bitsNA = ('a,bool list)na syntax "##" :: 'a => 'a list set => 'a list set (infixr 65) -translations "x ## S" == "op # x `` S" +translations "x ## S" == "Cons x `` S" constdefs atom :: 'a => 'a bitsNA