HomeIsabelle/Phabricator
Configuration option "show_results"

General

  • 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.
User
Projects
None
Subscribers
None

Event Timeline