equal
deleted
inserted
replaced
1 (* Author: Johannes Hoelzl, TU Muenchen *) |
1 (* Author: Johannes Hoelzl, TU Muenchen *) |
2 |
2 |
3 header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *} |
3 header {* Formalization of a Countermeasure by Koepf & Duermuth 2009 *} |
4 |
4 |
5 theory Koepf_Duermuth_Countermeasure |
5 theory Koepf_Duermuth_Countermeasure |
6 imports Information Permutation |
6 imports Information "~~/src/HOL/Library/Permutation" |
7 begin |
7 begin |
8 |
8 |
9 lemma |
9 lemma |
10 fixes p u :: "'a \<Rightarrow> real" |
10 fixes p u :: "'a \<Rightarrow> real" |
11 assumes "1 < b" |
11 assumes "1 < b" |