changeset 65449 | c82e63b11b8b |
parent 60770 | 240563fbf41d |
child 69587 | 53982d5ec0bb |
--- a/src/ZF/IMP/Com.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/IMP/Com.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section \<open>Arithmetic expressions, boolean expressions, commands\<close> -theory Com imports Main begin +theory Com imports ZF begin subsection \<open>Arithmetic expressions\<close>