equal
deleted
inserted
replaced
123 fun merge data = Symtab.merge (K true) data |
123 fun merge data = Symtab.merge (K true) data |
124 ) |
124 ) |
125 |
125 |
126 structure DeflMapData = Named_Thms |
126 structure DeflMapData = Named_Thms |
127 ( |
127 ( |
128 val name = "domain_deflation" |
128 val name = @{binding domain_deflation} |
129 val description = "theorems like deflation a ==> deflation (foo_map$a)" |
129 val description = "theorems like deflation a ==> deflation (foo_map$a)" |
130 ) |
130 ) |
131 |
131 |
132 structure Map_Id_Data = Named_Thms |
132 structure Map_Id_Data = Named_Thms |
133 ( |
133 ( |
134 val name = "domain_map_ID" |
134 val name = @{binding domain_map_ID} |
135 val description = "theorems like foo_map$ID = ID" |
135 val description = "theorems like foo_map$ID = ID" |
136 ) |
136 ) |
137 |
137 |
138 fun add_rec_type (tname, bs) = |
138 fun add_rec_type (tname, bs) = |
139 Rec_Data.map (Symtab.insert (K true) (tname, bs)) |
139 Rec_Data.map (Symtab.insert (K true) (tname, bs)) |