267 |
267 |
268 (*WN060728 strange behaviour: |
268 (*WN060728 strange behaviour: |
269 ### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ... |
269 ### fun the_hier reports these not overwritten ?!?...(stored twice ?!?) ... |
270 |
270 |
271 val it = () : unit |
271 val it = () : unit |
272 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"] |
272 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"] |
273 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"] |
273 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"] |
274 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"] |
274 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_minus1"] |
275 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"] |
275 *** insert: preserved ["Isabelle","RealBin","Theorems","real_mult_2"] |
276 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_assoc"] |
276 *** insert: preserved ["Isabelle","RealDef","Theorems","mult_assoc"] |
277 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"] |
277 *** insert: preserved ["Isabelle","RealDef","Theorems","real_mult_minus_eq1"] |
278 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"] |
278 *** insert: preserved ["Isabelle","RealDef","Theorems","add_assoc"] |
279 *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"] |
279 *** insert: preserved ["Isabelle","RealDef","Theorems","real_minus_divide_eq"] |
280 *** insert: preserved ["IsacScripts","ListG","Theorems","induct"] |
280 *** insert: preserved ["IsacScripts","ListG","Theorems","induct"] |
281 *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"] |
281 *** insert: preserved ["IsacScripts","ListG","Theorems","simps_1"] |