Changeset 2993 for src/ASM/Interpret2.ma
- Timestamp:
- Mar 28, 2013, 9:56:26 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret2.ma
r2910 r2993 39 39 definition OC_preclassified_system: labelled_object_code → preclassified_system ≝ 40 40 λc:labelled_object_code. 41 let lcm ≝ load_code_memory … (oc c) in 41 42 mk_preclassified_system_of_abstract_status 42 43 labelled_object_code 43 44 (OC_abstract_status c) 44 (λst. return (execute_1 … st))45 (λst. return (execute_1 lcm … st)) 45 46 (initialise_status … (load_code_memory (oc c))). 46 47
Note: See TracChangeset
for help on using the changeset viewer.