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.
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
authorblanchet
Wed, 14 Jul 2021 14:24:55 +0200
changeset 73978 906ecb049141
parent 73977 2d8a0f8e30ec
child 73979 e5322146e7e8
rephrase Nitpick constraint in more first-order format that's also more friendly to the 'box' option
src/HOL/Tools/Nitpick/nitpick_hol.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jul 14 10:02:43 2021 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jul 14 14:24:55 2021 +0200
@@ -2058,8 +2058,9 @@
        (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
             s_betapply [] (optimized_case_def hol_ctxt [] T bool_T (map case_func xs), x_var)),
         bisim_const T $ n_var $ x_var $ y_var),
-     HOLogic.eq_const pred_T $ (bisim_const T $ bisim_max $ x_var)
-     $ Abs (Name.uu, T, HOLogic.mk_eq (x_var, Bound 0))]
+     HOLogic.mk_imp
+       (bisim_const T $ bisim_max $ x_var $ y_var,
+        HOLogic.mk_eq (x_var, y_var))]
     |> map HOLogic.mk_Trueprop
   end
isabelle