equal
deleted
inserted
replaced
|
1 (* Title: HOL/IMP/Compiler.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, TUM |
|
4 Copyright 1996 TUM |
|
5 |
|
6 A simple compiler for a simplistic machine. |
|
7 *) |
|
8 |
1 theory Compiler = Natural: |
9 theory Compiler = Natural: |
2 |
10 |
3 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
11 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
4 |
12 |
5 consts stepa1 :: "instr list => ((state*nat) * (state*nat))set" |
13 consts stepa1 :: "instr list => ((state*nat) * (state*nat))set" |