Changeset 2492


Ignore:
Timestamp:
Nov 26, 2012, 11:52:51 AM (7 years ago)
Author:
campbell
Message:

Reduce axiomatisation in compiler.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2475 r2492  
    1818(* Recent changes have temporarily stopped the back-end from checking, so
    1919   axiomatise it for a little while.
    20 include "RTLabs/RTLabsToRTL.ma".
     20include "RTLabs/RTLabsToRTL.ma". *) include "RTL/RTL.ma". axiom rtlabs_to_rtl: RTLabs_program → rtl_program.
    2121include "RTL/RTLToERTL.ma".
    2222include "ERTL/ERTLToLTL.ma".
     
    3535  let p ≝ ltl_to_lin p in
    3636          lin_to_asm p.
    37 *)
    38 include "ASM/ASM.ma".
    39 axiom back_end : RTLabs_program → pseudo_assembly_program.
    4037
    4138include "ASM/Assembly.ma".
Note: See TracChangeset for help on using the changeset viewer.