changeset 362 | e51c9a67a68d |
parent 359 | fedc16924b76 |
--- a/thys/BitCoded2.thy Thu Feb 25 22:46:58 2021 +0000 +++ b/thys/BitCoded2.thy Sun Oct 10 00:56:47 2021 +0100 @@ -173,6 +173,8 @@ | "intern (STAR r) = ASTAR [S] (intern r)" + + fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where "retrieve (AONE bs) Void = bs" | "retrieve (ACHAR bs c) (Char d) = bs"