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/SMT/z3_replay_methods.ML
changeset 74382 8d0294d877bd
parent 72458 b44e894796d5 
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 22:12:52 2021 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Tue Sep 28 22:14:02 2021 +0200
@@ -315,10 +315,10 @@
   (thm COMP_INCR intro_hyp_rule1)
   handle THM _ => thm COMP_INCR intro_hyp_rule2
 
-fun negated_prop (\<^const>\<open>HOL.Not\<close> $ t) = HOLogic.mk_Trueprop t
+fun negated_prop \<^Const_>\<open>Not for t\<close> = HOLogic.mk_Trueprop t
   | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
 
-fun intro_hyps tab (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) cx =
+fun intro_hyps tab (t as \<^Const_>\<open>HOL.disj\<close> $ t1 $ t2) cx =
       lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
   | intro_hyps tab t cx =
       lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
@@ -376,7 +376,7 @@
 
 fun def_axiom_disj ctxt t =
   (case dest_prop t of
-    \<^const>\<open>HOL.disj\<close> $ u1 $ u2 =>
+    \<^Const_>\<open>disj for u1 u2\<close> =>
       SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (
          SMT_Replay_Methods.abstract_prop u2 ##>>  SMT_Replay_Methods.abstract_prop u1 #>>
          HOLogic.mk_disj o swap)
isabelle