/src/HOL/MicroJava/BV/
drwxr-xr-x [up]
-rw-r--r-- 2025-03-26 21:11 +0000 2564 Altern.thy
-rw-r--r-- 2025-03-26 21:11 +0000 18120 BVExample.thy
-rw-r--r-- 2025-03-26 21:11 +0000 15959 BVNoTypeError.thy
-rw-r--r-- 2025-03-26 21:11 +0000 5319 BVSpec.thy
-rw-r--r-- 2025-03-26 21:11 +0000 50026 BVSpecTypeSafe.thy
-rw-r--r-- 2025-03-26 21:11 +0000 12296 Correct.thy
-rw-r--r-- 2025-03-26 21:11 +0000 16760 Effect.thy
-rw-r--r-- 2025-03-26 21:11 +0000 12719 EffectMono.thy
-rw-r--r-- 2025-03-26 21:11 +0000 10404 JType.thy
-rw-r--r-- 2025-03-26 21:11 +0000 10581 JVM.thy
-rw-r--r-- 2025-03-26 21:11 +0000 16020 JVMType.thy
-rw-r--r-- 2025-03-26 21:11 +0000 12106 LBVJVM.thy
-rw-r--r-- 2025-03-26 21:11 +0000 9235 Typing_Framework_JVM.thy