Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/Comp/CorrCompTp.thy
changeset 15481 fc075ae929e4
parent 15236 f289e8ba2bb3
child 15781 70d559802ae3 
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -3,7 +3,9 @@
     Author:     Martin Strecker
 *)
 
-theory CorrCompTp =  LemmasComp + JVM + TypeInf + Altern:
+theory CorrCompTp
+imports LemmasComp TypeInf "../BV/JVM" "../BV/Altern"
+begin
 
 declare split_paired_All [simp del]
 declare split_paired_Ex [simp del]
isabelle