Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform operations wrt. Thm.full_prop_of;
authorwenzelm
Fri, 21 Apr 2023 15:30:59 +0200
changeset 77901 5728d5ebce34
parent 77900 42214742b44a
child 77902 01d6b2a44df8
more uniform operations wrt. Thm.full_prop_of;
src/HOL/Analysis/measurable.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:26:11 2023 +0200
+++ b/src/HOL/Analysis/measurable.ML	Fri Apr 21 15:30:59 2023 +0200
@@ -54,7 +54,7 @@
     (*cong_thms*) thm Item_Net.T *
     (string * preprocessor) list
   val empty: T =
-    (Item_Net.init eq_measurable_thm (single o Thm.prop_of o fst), Thm.item_net, Thm.item_net, [])
+    (Item_Net.init eq_measurable_thm (single o Thm.full_prop_of o fst), Thm.item_net, Thm.item_net, [])
   fun merge
    ((measurable_thms1, dest_thms1, cong_thms1, preprocessors1),
     (measurable_thms2, dest_thms2, cong_thms2, preprocessors2)) : T =
@@ -82,7 +82,7 @@
 
 fun del_thm th net =
   let
-    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
+    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm_prop (th, th'))
   in fold Item_Net.remove thms net end ;
 
 fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
isabelle