# HG changeset patch # User kleing # Date 966269306 -7200 # Node ID ec388b0a4eaaebd8121006bfec0c368d093eb673 # Parent 42d11e0a7a8b40799da76cb87bdc8712321f2a70 added MicroJava/BV/StepMono.thy, converted MicroJava/BV/Convert.thy to Isar diff -r 42d11e0a7a8b -r ec388b0a4eaa src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Aug 14 18:03:19 2000 +0200 +++ b/src/HOL/IsaMakefile Mon Aug 14 18:08:26 2000 +0200 @@ -363,7 +363,7 @@ MicroJava/JVM/Store.thy MicroJava/JVM/Store.ML \ MicroJava/BV/BVSpec.thy MicroJava/BV/Step.thy\ MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/BVSpecTypeSafe.ML \ - MicroJava/BV/Convert.thy MicroJava/BV/Convert.ML \ + MicroJava/BV/Convert.thy MicroJava/BV/StepMono.thy \ MicroJava/BV/Correct.thy MicroJava/BV/Correct.ML \ MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \ MicroJava/BV/LBVComplete.thy \