equal
deleted
inserted
replaced
41 lemmas [domain_deflation] = |
41 lemmas [domain_deflation] = |
42 deflation_upper_map deflation_lower_map deflation_convex_map |
42 deflation_upper_map deflation_lower_map deflation_convex_map |
43 |
43 |
44 setup {* |
44 setup {* |
45 fold Domain_Isomorphism.add_type_constructor |
45 fold Domain_Isomorphism.add_type_constructor |
46 [(@{type_name "upper_pd"}, @{term upper_defl}, @{const_name upper_map}), |
46 [(@{type_name "upper_pd"}, @{const_name upper_defl}, @{const_name upper_map}, [true]), |
47 (@{type_name "lower_pd"}, @{term lower_defl}, @{const_name lower_map}), |
47 (@{type_name "lower_pd"}, @{const_name lower_defl}, @{const_name lower_map}, [true]), |
48 (@{type_name "convex_pd"}, @{term convex_defl}, @{const_name convex_map})] |
48 (@{type_name "convex_pd"}, @{const_name convex_defl}, @{const_name convex_map}, [true])] |
49 *} |
49 *} |
50 |
50 |
51 end |
51 end |