Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/mutual.ML
changeset 70479 02d08d0ba896
parent 67149 e61557884799
child 81519 cdc43c0fdbfc 
--- a/src/HOL/Tools/Function/mutual.ML	Wed Aug 07 10:31:54 2019 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Aug 07 10:42:34 2019 +0200
@@ -263,6 +263,7 @@
     |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
     |> Thm.forall_intr x
     |> Thm.forall_intr P
+    |> Thm.solve_constraints
   end
isabelle