equal
deleted
inserted
replaced
390 in |
390 in |
391 (*Updating theory components: simprules and datatype info*) |
391 (*Updating theory components: simprules and datatype info*) |
392 (thy1 |> Theory.add_path big_rec_base_name |
392 (thy1 |> Theory.add_path big_rec_base_name |
393 |> PureThy.add_thmss [(("simps", simps), |
393 |> PureThy.add_thmss [(("simps", simps), |
394 [Simplifier.simp_add_global])] |
394 [Simplifier.simp_add_global])] |
395 |> PureThy.add_thmss [(("intrs", intrs), |
395 |> PureThy.add_thmss [(("", intrs), |
|
396 (*not "intrs" to avoid the warning that they |
|
397 are already stored by the inductive package*) |
396 [Classical.safe_intro_global])] |
398 [Classical.safe_intro_global])] |
397 |> DatatypesData.put |
399 |> DatatypesData.put |
398 (Symtab.update |
400 (Symtab.update |
399 ((big_rec_name, dt_info), DatatypesData.get thy1)) |
401 ((big_rec_name, dt_info), DatatypesData.get thy1)) |
400 |> ConstructorsData.put |
402 |> ConstructorsData.put |