equal
deleted
inserted
replaced
1 theory IMP_3 |
1 theory IMP_3 |
2 imports "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
2 imports "HOL-Library.Predicate_Compile_Quickcheck" |
3 begin |
3 begin |
4 |
4 |
5 subsection \<open>IMP\<close> |
5 subsection \<open>IMP\<close> |
6 |
6 |
7 text \<open> |
7 text \<open> |