Changeset 2129 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jun 27, 2012, 7:14:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2124 r2129 400 400 status_of_pseudo_status M' cm s sigma policy). 401 401 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 402 cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *) 403 (* 402 404 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 403 405 #costs #create_label_cost_refl #newppc … … 1371 1373 (* XXX: finally, prove the equality using sigma commutation *) 1372 1374 cases daemon 1373 ] 1374 qed. 1375 ] *) 1376 qed.
Note: See TracChangeset
for help on using the changeset viewer.