On Sun, 8 Jan 2012, Alexander Krauss wrote:
On 01/05/2012 12:19 PM, Jasmin Christian Blanchette wrote:
We are not allowed to distribute Yices. When publishing the components,
please exclude Yices.
... and Vampire.
Could we instead provide a little script (or Isabelle tool) that turns a
There is another drop-out concerning 'a set (in Isabelle/05a82dd869ed):
inductive_set
well_formed_gterm' :: ('f \Rightarrow nat) \Rightarrow 'f gterm set
for arity :: 'f \Rightarrow nat
where
step[intro!]: \lbrakkargs \in lists (well_formed_gterm' arity);
length args = arity
Does the old src/HOLCF/IsaMakefile still have any purpose?
Ever since the inclusion of HOLCF within the regular HOL session library
it should be subsumed by the main src/HOL/IsaMakefile. Some recent
changes appy to both files nonetheless, see
Quoting Lawrence Paulson l...@cam.ac.uk:
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
