# HG changeset patch # User bulwahn # Date 1333088369 -7200 # Node ID ac625d8346b2e5b30d7c72c97afe3346b0d58f5e # Parent 06e6f352df1bff3fddc90edfa1b9a88d0e674edb hiding fact not so aggressively diff -r 06e6f352df1b -r ac625d8346b2 src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 30 00:01:30 2012 +0100 +++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Mar 30 08:19:29 2012 +0200 @@ -587,7 +587,7 @@ use "Tools/Quickcheck/abstract_generators.ML" -hide_fact orelse_def +hide_fact (open) orelse_def no_notation orelse (infixr "orelse" 55) hide_fact