[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'

[Alexander Krauss]

Stefan Berghofer wrote:
>   inductive foo :: "'a => 'a => bool"
>   where
>     "foo x x"
> 
>   locale test =
>     fixes t P
>     assumes ensure_clash [simp]: "t = P"
>   begin
> 
>   inductive_cases bar: "foo t z"

Nice. :-)