Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
authornipkow
Thu, 26 Oct 2000 14:59:38 +0200
changeset 10343 24c87e1366d8
parent 10342 b124d59f7b61
child 10344 bb0b65380516
*** empty log message ***
src/HOL/IMP/Compiler.thy file | annotate | diff | comparison | revisions
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:52:41 2000 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Oct 26 14:59:38 2000 +0200
@@ -1,3 +1,11 @@
+(*  Title:      HOL/IMP/Compiler.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, TUM
+    Copyright   1996 TUM
+
+A simple compiler for a simplistic machine.
+*)
+
 theory Compiler = Natural:
 
 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
--- a/src/HOL/IsaMakefile	Thu Oct 26 14:52:41 2000 +0200
+++ b/src/HOL/IsaMakefile	Thu Oct 26 14:59:38 2000 +0200
@@ -198,7 +198,7 @@
 
 HOL-IMP: HOL $(LOG)/HOL-IMP.gz
 
-$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
+$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler.thy IMP/Denotation.ML \
   IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
   IMP/Natural.ML IMP/Natural.thy IMP/Examples.ML IMP/Examples.thy \
   IMP/Transition.ML IMP/Transition.thy IMP/VC.ML IMP/VC.thy IMP/ROOT.ML
isabelle