exit 1
T.thy:6:4: spelled-out-notation: widen is written out; its notation is _ \<nabla> _ [*]
T.thy:6:13: spelled-out-notation: widen is written out; its notation is _ \<nabla> _ [*]
T.thy:6:30: spelled-out-notation: get is written out; its notation is _\<langle>_\<rangle> [*]
T.thy:6:56: spelled-out-notation: gamma_int is written out; it is overloaded as gamma [*]
T.thy:6:70: spelled-out-abbreviation: step (f y) (f y) is written out; it is the abbreviation twice [*]
T.thy:7:3: unfinished-proof: sorry leaves the goal unproved
T.thy:11:22: spelled-out-notation: widen is written out; its notation is _ \<nabla> _ [*]
T.thy:11:45: redundant-brackets: (gamma_int) needs no brackets [*]
T.thy:11:66: unfinished-proof: sorry leaves the goal unproved
T.thy:16:4: spelled-out-notation: eval is written out; its notation is \<lbrakk>_\<rbrakk>\<^sup>\<sharp> [*]
T.thy:16:21: spelled-out-notation: eval is written out; its notation is \<lbrakk>_\<rbrakk>\<^sup>\<sharp> [*]
T.thy:16:37: spelled-out-notation: eval is written out; its notation is \<lbrakk>_\<rbrakk>\<^sup>\<sharp> [*]
T.thy:16:43: redundant-brackets: (a) needs no brackets [*]
T.thy:16:49: redundant-brackets: (b) needs no brackets [*]
T.thy:16:58: spelled-out-notation: eval is written out; its notation is \<lbrakk>_\<rbrakk>\<^sup>\<sharp> [*]
T.thy:16:70: spelled-out-notation: tight is written out; its notation is \<lfloor>_\<rfloor> [*]
T.thy:17:3: unfinished-proof: sorry leaves the goal unproved
--- stderr
fixed 0 findings
17 findings: 10 spelled-out-notation, 3 redundant-brackets, 3 unfinished-proof, 1 spelled-out-abbreviation
14 with --fix=all
