#2112 (Jan 30, 2024, 1:36:05 AM)

1. merged (detail / hgweb)
2. define_time_function: avoid unused let's (detail / hgweb)
3. common type class for trivial properties on div/mod (detail / hgweb)
4. more robust (amending 1600fb749c54), to support the following corner case:
     schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))"
       apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>)
       oops (detail / hgweb)

Started by an SCM change

This run spent:

• 46 min waiting;
• 2 hr 2 min build duration;
• 2 hr 48 min total from scheduled to completion.