Quoting Lawrence Paulson :
I got this message several times when converting theories. There is
a workaround, but nevertheless, I think this is a bug.
Hi Larry,
the reason for this problem is the removal of the rules pred_equals_eq and
pred_subset_eq from the rule database used for the predica
I got this message several times when converting theories. There is a
workaround, but nevertheless, I think this is a bug.
Larry
On 9 Jan 2012, at 13:31, Makarius wrote:
> There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
>
> inductive_set
> well_formed_gterm' :: "('f \ n
There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
inductive_set
well_formed_gterm' :: "('f \ nat) \ 'f gterm set"
for arity :: "'f \ nat"
where
step[intro!]: "\args \ lists (well_formed_gterm' arity);
length args = arity f\
\ (Apply f args)
