# HG changeset patch # User wenzelm # Date 1632305039 -7200 # Node ID 4974c3697fee0e63f9f56e09fab92a019db45579 # Parent cdf8952a86d5e38610baa057eaca52ec233bcb0e proper NEWS; diff -r cdf8952a86d5 -r 4974c3697fee NEWS --- a/NEWS Wed Sep 22 11:58:45 2021 +0200 +++ b/NEWS Wed Sep 22 12:03:59 2021 +0200 @@ -20,7 +20,7 @@ in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this: - context notes [[show_results = true]] + context notes [[show_results = false]] begin definition "test = True" theorem test by (simp add: test_def)