| changeset 10834 | a7897aebbffc |
| parent 8732 | aef229ca5e77 |
| child 12792 | b344226f924c |
--- a/src/HOL/Lex/RegExp2NAe.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOL/Lex/RegExp2NAe.thy Tue Jan 09 15:32:27 2001 +0100 @@ -12,7 +12,7 @@ types 'a bitsNAe = ('a,bool list)nae syntax "##" :: 'a => 'a list set => 'a list set (infixr 65) -translations "x ## S" == "Cons x `` S" +translations "x ## S" == "Cons x ` S" constdefs atom :: 'a => 'a bitsNAe