[isabelle-dev] NEWS: Configuration option "show_results"

Makarius makarius at sketis.net
Wed Sep 22 12:27:12 CEST 2021


*** 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 = false]]
  begin
    definition "test = True"
    theorem test by (simp add: test_def)
  end


This refers to Isabelle/4974c3697fee.

It is mainly relevant for benchmarks or really big arrays of definitions and
theorems, where printing takes considerable time.


	Makarius


More information about the isabelle-dev mailing list