Mercurial Mercurial > hg > lexing / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/BitCodedCT.thy
changeset 400 46e5566ad4ba
parent 346 f1feb44adfe1 
--- a/thys/BitCodedCT.thy	Sat Jan 29 16:43:51 2022 +0000
+++ b/thys/BitCodedCT.thy	Sat Jan 29 23:53:21 2022 +0000
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
lexing