Email Gateway (Sep 22 2021 at 10:27): Email Gateway (Sep 22 2021 at 10:27):From: Makarius <makarius@sketis.net>
* 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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC