# HG changeset patch # User Cezary Kaliszyk # Date 1283151129 -32400 # Node ID 2795499a20bdb02080c48c2e1da6e27b52810b1b # Parent 27c7b620758cf0e972fba22428afd15cf09a2bed Quotient Package: dont unfold mem_def, use rsp and prs instead diff -r 27c7b620758c -r 2795499a20bd src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 15:44:33 2010 +0900 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 15:52:09 2010 +0900 @@ -619,10 +619,10 @@ (* Since we use Ball and Bex during the lifting and descending, - we cannot deal with lemmas containing them, unless we unfold - them by default. Also mem cannot be regularized in general. *) + we cannot deal with lemmas containing them, unless we unfold + them by default. *) -val default_unfolds = @{thms Ball_def Bex_def mem_def} +val default_unfolds = @{thms Ball_def Bex_def} (** descending as tactic **)