1.1 --- a/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:52:41 2000 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:59:38 2000 +0200
     1.3 @@ -1,3 +1,11 @@
     1.4 +(*  Title:      HOL/IMP/Compiler.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow, TUM
     1.7 +    Copyright   1996 TUM
     1.8 +
     1.9 +A simple compiler for a simplistic machine.
    1.10 +*)
    1.11 +
    1.12  theory Compiler = Natural:
    1.13  
    1.14  datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat

     2.1 --- a/src/HOL/IsaMakefile	Thu Oct 26 14:52:41 2000 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Thu Oct 26 14:59:38 2000 +0200
     2.3 @@ -198,7 +198,7 @@
     2.4  
     2.5  HOL-IMP: HOL $(LOG)/HOL-IMP.gz
     2.6  
     2.7 -$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
     2.8 +$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy IMP/Denotation.ML \
     2.9    IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
    2.10    IMP/Natural.ML IMP/Natural.thy IMP/Examples.ML IMP/Examples.thy \
    2.11    IMP/Transition.ML IMP/Transition.thy IMP/VC.ML IMP/VC.thy IMP/ROOT.ML