NEWS
changeset 74349 4974c3697fee
parent 74348 cdf8952a86d5
child 74364 99add5178e51
child 74365 b49bd5d9041f
equal deleted inserted replaced
74348:cdf8952a86d5 74349:4974c3697fee
    18 * Configuration option "show_results" controls output of final results
    18 * Configuration option "show_results" controls output of final results
    19 in commands like 'definition' or 'theorem'. Output is normally enabled
    19 in commands like 'definition' or 'theorem'. Output is normally enabled
    20 in interactive mode, but it could occasionally cause unnecessary
    20 in interactive mode, but it could occasionally cause unnecessary
    21 slowdown. It can be disabled like this:
    21 slowdown. It can be disabled like this:
    22 
    22 
    23   context notes [[show_results = true]]
    23   context notes [[show_results = false]]
    24   begin
    24   begin
    25     definition "test = True"
    25     definition "test = True"
    26     theorem test by (simp add: test_def)
    26     theorem test by (simp add: test_def)
    27   end
    27   end
    28 
    28