Changeset 1515 for src/ASM/StatusProofs.ma
- Timestamp:
- Nov 18, 2011, 1:03:14 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/StatusProofs.ma
r1014 r1515 182 182 lemma get_8051_sfr_write_at_stack_pointer: 183 183 ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y. 184 #T #s #x #y whd in ⊢ (??%%) //184 #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl 185 185 qed. 186 186
Note: See TracChangeset
for help on using the changeset viewer.