changeset 69605 | a96320074298 |
parent 67399 | eab6ce8368fa |
69604:d80b2df54d31 | 69605:a96320074298 |
---|---|
41 shows "Rel_match B (f x) (g y)" |
41 shows "Rel_match B (f x) (g y)" |
42 using assms Rel_match_Rel Rel_app Rel_Rel_match by fast |
42 using assms Rel_match_Rel Rel_app Rel_Rel_match by fast |
43 |
43 |
44 end |
44 end |
45 |
45 |
46 ML_file "conditional_parametricity.ML" |
46 ML_file \<open>conditional_parametricity.ML\<close> |
47 |
47 |
48 end |
48 end |