equal
deleted
inserted
replaced
1 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
1 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
2 notation ( output) "Trueprop" ("#_" [1000] 1000) |
2 notation ( output) "Trueprop" ("#_" [1000] 1000) |
|
3 |
|
4 lemma regularize_to_injection: |
|
5 shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
|
6 by(auto simp add: QUOT_TRUE_def) |
|
7 |
|
8 |
|
9 |
3 |
10 |
4 ML {* |
11 ML {* |
5 fun dest_cbinop t = |
12 fun dest_cbinop t = |
6 let |
13 let |
7 val (t2, rhs) = Thm.dest_comb t; |
14 val (t2, rhs) = Thm.dest_comb t; |