Ignore:
Timestamp:
Jun 28, 2012, 6:47:26 PM (8 years ago)
Author:
mulligan
Message:

Done the hardest cases in the main theorem. Just got a few daemons to close...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2139 r2140  
    403403                      status_of_pseudo_status M' cm s sigma policy).
    404404    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
     405  (* XXX: takes about 45 minutes to type check! *)
    405406  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
    406407  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
Note: See TracChangeset for help on using the changeset viewer.