equal
deleted
inserted
replaced
144 declare [[map list = (map, LIST_REL)]] |
144 declare [[map list = (map, LIST_REL)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
145 declare [[map * = (prod_fun, prod_rel)]] |
146 declare [[map "fun" = (fun_map, FUN_REL)]] |
146 declare [[map "fun" = (fun_map, FUN_REL)]] |
147 |
147 |
148 lemmas [quotient_thm] = |
148 lemmas [quotient_thm] = |
149 FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT |
149 FUN_QUOTIENT LIST_QUOTIENT |
150 |
150 |
151 ML {* maps_lookup @{theory} "List.list" *} |
151 ML {* maps_lookup @{theory} "List.list" *} |
152 ML {* maps_lookup @{theory} "*" *} |
152 ML {* maps_lookup @{theory} "*" *} |
153 ML {* maps_lookup @{theory} "fun" *} |
153 ML {* maps_lookup @{theory} "fun" *} |
154 |
154 |