Configuration option "show_results"
- Configuration option "show_results" controls output of final results in commands like 'definition' or 'theorem'. Output is normally enabled in interactive mode, but it could occasionally cause unnecessary slowdown. It can be disabled like this:
context notes [[show_results = true]] begin definition "test = True" theorem test by (simp add: test_def) end
This refers to Isabelle/4974c3697fee.
Written by makarius on Sep 22 2021, 12:04 PM.