equal
deleted
inserted
replaced
129 fun add_deflation_thm thm = |
129 fun add_deflation_thm thm = |
130 Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm) |
130 Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm) |
131 |
131 |
132 val get_rec_tab = Rec_Data.get |
132 val get_rec_tab = Rec_Data.get |
133 fun get_deflation_thms thy = |
133 fun get_deflation_thms thy = |
134 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation} |
134 rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}) |
135 |
135 |
136 val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID} |
136 val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID} |
137 fun get_map_ID_thms thy = |
137 fun get_map_ID_thms thy = |
138 Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID} |
138 rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}) |
139 |
139 |
140 |
140 |
141 (******************************************************************************) |
141 (******************************************************************************) |
142 (************************** building types and terms **************************) |
142 (************************** building types and terms **************************) |
143 (******************************************************************************) |
143 (******************************************************************************) |