Be less verbose
[isa-where-to-move.git] / Where_To_Move_Ex4.thy
1 theory Where_To_Move_Ex4
2 imports Where_To_Move_Ex3 Where_To_Move 
3 begin
4
5 lemma fooI2: "foo" by (rule fooI)
6 lemma barE2: "bar \<Longrightarrow> P" by (rule barE)
7 lemma foobar: "foo \<and> \<not> bar"
8   apply rule
9   apply (rule fooI)
10   apply (rule notI)
11   apply (erule barE)
12   done
13 lemma foobar2: "foo \<and> \<not> bar"
14   apply rule
15   apply (rule fooI2)
16   apply (rule notI)
17   apply (erule barE2)
18   done
19
20 where_to_move
21 where_to_move foobar2
22
23 end