changeset 18 | d826899bc424 |
parent 6 | 38cef5407d82 |
17:86918b45b2e6 | 18:d826899bc424 |
---|---|
1 theory TM_Assemble |
1 theory TM_Assemble |
2 imports Hoare_tm StateMonad AList |
2 imports Hoare_tm StateMonad |
3 "~~/src/HOL/Library/FinFun_Syntax" |
3 "~~/src/HOL/Library/FinFun_Syntax" |
4 "~~/src/HOL/Library/Sublist" |
4 "~~/src/HOL/Library/Sublist" |
5 LetElim |
5 LetElim |
6 begin |
6 begin |
7 |
7 |