equal
deleted
inserted
replaced
3 |
3 |
4 lemma regularize_to_injection: |
4 lemma regularize_to_injection: |
5 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
5 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
6 by(auto simp add: QUOT_TRUE_def) |
6 by(auto simp add: QUOT_TRUE_def) |
7 |
7 |
|
8 syntax |
|
9 "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10) |
|
10 translations |
|
11 "\<exists>!!x\<in>A. P" == "Bexeq A (%x. P)" |
8 |
12 |
9 |
13 |
10 (* Atomize infrastructure *) |
14 (* Atomize infrastructure *) |
11 (* FIXME/TODO: is this really needed? *) |
15 (* FIXME/TODO: is this really needed? *) |
12 (* |
16 (* |