equal
deleted
inserted
replaced
1 theory BlexerSimp |
1 theory BlexerSimp |
2 imports Blexer |
2 imports Blexer |
3 begin |
3 begin |
4 |
|
5 |
|
6 lemma test: |
|
7 assumes "Q \<Longrightarrow> P" |
|
8 shows "~P \<Longrightarrow> ~Q" |
|
9 using assms |
|
10 apply(erule_tac contrapos_nn) |
|
11 apply(simp) |
|
12 done |
|
13 |
4 |
14 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list" |
5 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list" |
15 where |
6 where |
16 "distinctWith [] eq acc = []" |
7 "distinctWith [] eq acc = []" |
17 | "distinctWith (x # xs) eq acc = |
8 | "distinctWith (x # xs) eq acc = |