Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. define_time_function: avoid unused let's
  3. common type class for trivial properties on div/mod
  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
Changeset 79543:bbed18f7a522 by nipkow:
merged
Changeset 79542:b941924a407d by nipkow:
define_time_function: avoid unused let&#039;s
The file was modified src/HOL/Data_Structures/Define_Time_Function.ML (diff)
Changeset 79541:4f40225936d1 by haftmann:
common type class for trivial properties on div/mod
The file was modified src/HOL/Bit_Operations.thy (diff)
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Fields.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 79540:afa75b58166a by wenzelm:
more robust (amending 1600fb749c54), to support the following corner case:<br>&nbsp; schematic_goal &quot;PROP ((?f :: ?&#039;a \&lt;Rightarrow&gt; _) (x :: ?&#039;a))&quot;<br>&nbsp;&nbsp;&nbsp; apply (tactic \&lt;open&gt;PRIMITIVE (Thm.instantiate (TVars.make1 (((&quot;&#039;a&quot;, 0), []), @{ctyp prop}), Vars.empty))\&lt;close&gt;)<br>&nbsp;&nbsp;&nbsp; oops
The file was modified src/Pure/Isar/proof_display.ML (diff)