Re: [isabelle] Weird nesting of Quantifiers

To: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: [isabelle] Weird nesting of Quantifiers
From: Peter Lammich <lammich at in.tum.de>
Date: Tue, 16 Feb 2021 12:26:58 +0000
Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
In-reply-to: <9DC20E87-8E37-4F2D-B22B-2224CB404032@cam.ac.uk>
References: <53699b30cd2bda58ebb26792bacc4e37ac66d5e0.camel@in.tum.de> <9DC20E87-8E37-4F2D-B22B-2224CB404032@cam.ac.uk>
User-agent: Evolution 3.36.4-0ubuntu1

Thanks Larry and Thomas, that works a treat for my examples!

--
  Peter


On Mon, 2021-02-15 at 10:36 +0000, Lawrence Paulson wrote:
> Try this:
> 
> 	apply (simp flip: ex_simps all_simps)
> 
>

References:
- [isabelle] Weird nesting of Quantifiers
  - From: Peter Lammich
- Re: [isabelle] Weird nesting of Quantifiers
  - From: Lawrence Paulson

Previous by Date: Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer
Next by Date: [isabelle] Conflict of type arities: What are the constraints on class instantiations?
Previous by Thread: Re: [isabelle] Weird nesting of Quantifiers
Next by Thread: [isabelle] Isabelle2021-RC6 available for applications
Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
Cl-isabelle-users list archive Table of Contents
More information about the Cl-isabelle-users mailing list

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.