Hi all,
I just noticed that the integral syntax defined in [1] can be used to
trigger some system-level exception: If, instead of the correct
\<integral> x. f x \<partial> y
I write
\<integral> x x'. f x \<partial> y
Isabelle prints
exception TERM raised (line 141 of "Syntax/syntax_trans.ML"): abs_tr
-- Lars.
[1] src/HOL/Probability/Lebesgue_Integration.thy, lines 1688ff
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
