[isabelle-dev] NEWS (constant ii)

* Renamed ii to imaginary_unit in order to free up ii as a variable name. The syntax \ remains available. INCOMPATIBILITY. To my surprise, there are thousands of occurrences of ii throughout the library than the AFP. The overwhelming majority of these have nothing to do with the complex

Re: [isabelle-dev] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

Is it time to implement this change, regarding the imaginary constant ii? Note: I have no suggestions for improving the star notation of non-standard analysis, mentioned in the last paragraph. Larry Paulson > On 19 Nov 2016, at 19:48, Makarius wrote: > > Here is also

[isabelle-dev] The Great Picard Theorem

I have just added this to the Analysis directory, making its inevitable refactoring more necessary. Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently expert in complex analysis to say whether it is core material or not. It looks like a fundamental result to me. We should

Re: [isabelle-dev] Bitbucket SSH craziness escalates

gt;> On 21.02.2017, at 22:12, Lawrence Paulson <l...@cam.ac.uk >> <mailto:l...@cam.ac.uk>> wrote: >> >> I committed some changes (fixing AFP-devel), which I would like to push. But >> what in God’s name is this? >> >> ~/isabelle/afp/deve

[isabelle-dev] Bitbucket SSH craziness escalates

I committed some changes (fixing AFP-devel), which I would like to push. But what in God’s name is this? ~/isabelle/afp/devel/thys: hg push pushing to https://bitbucket.org/isa-afp/afp-devel searching for changes http authorization required realm:

Re: [isabelle-dev] A note on composition in src/Pure/library.ML

I’m not sure what to conclude from this. It’s about non-functional behaviour, so not quite something people ought to rely upon. I’m guessing one could make the change and nothing would happen. I’m still not convinced that the case for a change has been made however. For what it’s worth, there

[isabelle-dev] NEWS

* Session HOL-Analysis: more material involving arcs, paths, covering spaces, innessential maps, retracts. Major results include the Jordan Curve Theorem. ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] NEWS: PIDE document maintains file content internally

On 8 Jan 2017, at 19:02, Makarius wrote: > > * The PIDE document model maintains file content independently of the > status of jEdit editor buffers. Reloading jEdit buffers no longer causes > changes of formal document content. Theory dependencies are always > resolved

Re: [isabelle-dev] Integers in Poly/ML

Let’s be clear: the semantics of type int is well-defined. It denotes the set of integers over a specific finite range of values, and if this range is exceeded, exception Overflow is raised. If one’s requirements fit within that range of values then there is no rational reason to suffer a

Re: [isabelle-dev] Integers in Poly/ML

Just as remark: MetiTarski took a slight performance hit in the transition to the new compiler, happily greatly reversed by my decision to use fixed-precision integers. Of course I would like to use the IDE for Standard ML, but getting started is always more complicated than it looks. Larry

Re: [isabelle-dev] Integers in Poly/ML

gt; wrote: > > On 02/11/16 15:58, Lawrence Paulson wrote: >> I have to say, I’m absolutely mystified by the response to my suggestion. > > Why? I did not reject the idea, but only put it into the context of > Isabelle. MetiTarski is a small research experiment, but Isabelle a huge

Re: [isabelle-dev] Integers in Poly/ML

. No exception handlers had to be added when I converted MetiTarski to use fixed integers. An uncaught exception doesn’t prove anything, of course. Larry > On 2 Nov 2016, at 14:43, Makarius <makar...@sketis.net> wrote: > > On 02/11/16 15:30, Lawrence Paulson wrote: >> >

Re: [isabelle-dev] Integers in Poly/ML

The difference is substantial and uniform. I attach log files summarising MetiTarski’s performance by nearly 900 examples. You will note that total CPU time is way down, and problems consistently run much faster using fixed-precision arithmetic. Both runs involve the new version of Poly/ML,

[isabelle-dev] Integers in Poly/ML

David Matthews is working on a new release of Poly/ML in which the default type of integers is fixed-precision. A configuration option can restore the former set up, but that might be a mistake: I modified MetiTarski to use large integers only where needed and saw runtime decrease by around

[isabelle-dev] Damn

A slight disappointment this weekend. I thought I would have a proof of the Jordan curve theorem just in time for the release. All the prerequisites seemed to be there. Sledgehammer was proving the goals one after another. Even with the last goal, it proved half and suggested two proofs for the

Re: [isabelle-dev] Towards the release

I see no need for a (?) next to El Capitan. I’ve been using it on multiple machines for nearly a year. Larry > On 26 Oct 2016, at 10:58, Makarius wrote: > > On 26/10/16 00:05, gerwin.kl...@data61.csiro.au wrote: >> I’m planning to switch over to Sierra this week, and can

Re: [isabelle-dev] Old_Number_Theory

That is great news! It’s a pity that our coverage of number theory is minuscule compared with what we have for analysis. I blame John Harrison :-) Larry > On 18 Oct 2016, at 12:11, Manuel Eberl wrote: > > I am glad to announce that as of 261d42f0bfac, Old_Number_Theory is

Re: [isabelle-dev] Towards the release

That would be great! I believe that Gauss’s law of quadratic reciprocity and Wilson’s theorem were never ported To Number_Theory. Larry > On 13 Oct 2016, at 17:36, Manuel Eberl wrote: > > I for one am hoping to be able to get rid of the Old Number Theory > before the

Re: [isabelle-dev] Jenkins maintenance

I don’t agree with this point at all. Fixing the errors is easy but locating them certainly isn’t. I’m happy as long as somebody else is willing to do that. Larry > On 6 Oct 2016, at 14:02, Makarius wrote: > > * A broken Latex document is easy to repair.

Re: [isabelle-dev] Jenkins maintenance

I have wanted to keep out of this rather fraught discussion, but I agree on this issue. How dangerous it is depends on how critical those secrets are. And I’m perfectly aware that key management can be difficult and maybe there is little point if only one instance of this thing is running.

Re: [isabelle-dev] Jenkins maintenance

I have a Mac Pro, and I just use “isabelle build -a”. If I know that my changes affect specific AFP entries, I run them manually. A full test takes a couple of hours, and it is a pain. Maybe I could use multithreading more (the machine supports 12 cores). Larry > On 6 Oct 2016, at 13:05,

Re: [isabelle-dev] The HOL Light library

And now that I have managed to prove “invariance of domain”, a significant if not especially famous result. Larry > On 6 Oct 2016, at 14:08, Makarius wrote: > > Definitely. It is probably worth a line to the ANNOUNCE file for > Isabelle2016-1.

Re: [isabelle-dev] Fisher–Yates in AFP

Thanks and I have finally managed to push the entry. Unfortunately a problem like this seems to happen 30% of the time with new AFP entries… Larry > On 4 Oct 2016, at 12:23, Lars Hupel wrote: > >> If it’s no problem, maybe the submission system could check for such >>

Re: [isabelle-dev] Fisher–Yates in AFP

That is indeed the culprit. If it’s no problem, maybe the submission system could check for such directories and delete them? Larry > On 4 Oct 2016, at 12:18, Manuel Eberl wrote: > > Oh, that is quite possible. Sorry about that. I typically keep my prospective > AFP

Re: [isabelle-dev] Fisher–Yates in AFP

It isn’t only about SourceTree. As I mentioned, manually adding Fisher_Yates had no effect, and even now "hg diff” shows nothing, even though Fisher_Yates should appear as “added” or untracked (given that it’s on my machine and nowhere else). I’ve also checked every .hgignore file. Possibly my

Re: [isabelle-dev] Jenkins maintenance

I’d be happy with this, if it’s achievable. I’ve only tried the testboard once or twice; I find it too easy to do the wrong thing when you have a choice of targets to push to, and I have a powerful machine so I prefer to test there. But a mechanism of the sort you describe (provided it’s easy

[isabelle-dev] The HOL Light library

I’ve just added a lot more advanced material from HOL Light. There isn't much about this in the NEWS file; unfortunately there is no headline result to mention or even a dominant theme. Nor can we say that the entire library has been ported. But I still think it’s a significant development for

Re: [isabelle-dev] More HOL-Analysis

Please let me know when you move the file Continuum_Not_Denumerable.thy. I have quite a few theorems connected with cardinality and topological concepts. Possibly they should not be added to that theory and it should simply be included at some point in the development. Larry > On 16 Sep 2016,

Re: [isabelle-dev] More HOL-Analysis

Convex_Euclidean_Space is the largest file in Analysis, more than half a megabyte, so rather than combining the files it would be good to split them up even more. I admit, I have been putting in a lot of new material and trying to put things in sensible places, but with no global overview of

Re: [isabelle-dev] More HOL-Analysis

I’m continuing to port a lot of material from HOL Light, and indeed I’m going to need that exact theory very soon. Larry > On 16 Sep 2016, at 15:23, Makarius wrote: > > There seems to be an ongoing consolidation of HOL-Analysis (although the > NEWS are relatively terse

Re: [isabelle-dev] not-exists problem

The symmetry between the variables in ~(∃x y. P x y) is completely lost in ∄x. ∃y. P x y. It’s a terrible notation. Larry > On 13 Sep 2016, at 22:56, Jasmin Blanchette > wrote: > >> I’m not sure that this suggestion addresses my original problem: that the >> use

Re: [isabelle-dev] not-exists problem

I’m not sure that this suggestion addresses my original problem: that the use of the negated quantifier (by an output translation, i.e., not by request) produced a confusing output. This output already contains only a single variable bound by ∄. Larry > On 13 Sep 2016, at 19:56, Makarius

Re: [isabelle-dev] not-exists problem

When mathematicians use such notations, they are communicating informally and they can count on the reader to understand what they mean. But that’s not how it works for us. Any notation that could be misinterpreted should be input only (assuming we support it at all). That way, the user

[isabelle-dev] not-exists problem

We have a problem with the ∄ operator, when existential quantifiers are nested: lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" by (rule refl) Note that ∄x y. P x y would be fine. Larry ~/isabelle/Repos/src/HOL: hg id dca6fabd8060 tip ___ isabelle-dev

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

Thank you for making this change! > My idea would be to rename both integrals into something like: > has_bc_integral, bc_integrable, bc_integral, > has_hk_integral, hk_integrable, hk_integral > and consequently rename the integral theorems. I would greatly prefer renaming the relevant

Re: [isabelle-dev] multiplicity and prime numbers

The reason why we put x/0= 0 is because it simplifies the statements of many laws, not because of any admiration of 0. Larry > On 19 Jul 2016, at 11:24, Manuel Eberl wrote: > > The obvious possibility would be to just let all non-prime numbers have > multiplicity 0.

Re: [isabelle-dev] multiplicity and prime numbers

This is what I would do Larry Paulson > On 19 Jul 2016, at 11:03, Manuel Eberl wrote: > > 3. replace the old multilicity with the new one and adapt all lemmas > accordingly > > Currently, I tend towards the last options. Are there any other opinions on > this?

[isabelle-dev] \nexists

The recent failure in Multivariable_Analysis was caused by the \nexists macro, which is not defined: ! Undefined control sequence. \nexists The corresponding source line is here: Multivariate_Analysis/Brouwer_Fixpoint.thy:have nog: "\g. continuous_on (S \ connected_component_set (- S)

Re: [isabelle-dev] Use HTTPS for components

I’m not sure that digitally signed components are really something to work on now. Are we really concerned about malicious attacks against our servers? Larry > On 13 Jul 2016, at 00:56, Gerwin Klein wrote: > > I agree, we should do that. > > Ideally, we should

Re: [isabelle-dev] [Isabelle-ci] Build failure in Isabelle

I’m taking care of it Larry > On 16 Jun 2016, at 10:44, Manuel Eberl wrote: > > Sure, I can do that later today. ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

uld think. > > There are two more instances in Brouwer_Fixpoint.thy where you wrote > something like "R^n" in text, causing the same error. > > Cheers, > > Manuel > > >> On 15/06/16 18:19, Lawrence Paulson wrote: >> No idea what’s going on here. I did commit a lot of

[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle

No idea what’s going on here. I did commit a lot of stuff but it works on my machine. I added a theory, but the addition was committed and I have no untracked files. If anybody can figure out what’s going on I'd be grateful. I see it is a document preparation failure, presumably that isn’t

Re: [isabelle-dev] Whole word search

But what is the scope of this selection? The entire file or some local scope? Larry > On 6 Jun 2016, at 20:29, Makarius wrote: > > > Anyway, for the described application to rename the "x" within a lambda > expression, you can now use isabelle.select-entity as described in

[isabelle-dev] problem with Nominal in the AFP

Incompleteness FAILED (see also /media/data/jenkins/workspace/isabelle-repo-afp/heaps/polyml-5.6_x86_64-linux/log/Incompleteness) *** Specification.definition NONE [] ((permute_def_name, []), permute_eqn) *** : Attrib.binding * term -> *** local_theory -> (term * (string *

[isabelle-dev] Whole word search

There appear to have been some changes in policy concerning the meaning of “whole word” in jEdit find and replace. Let’s suppose that we want to rename the variable x in the expression λx. if P x then 1 else 0. For quite some time, the occurrence of x in “λx.” was not regarded as a “whole

Re: [isabelle-dev] Isabelle repository broken

I did run a full test of my changes, which in any event don’t look connected with the error message you report. Larry > On 24 May 2016, at 16:12, Makarius wrote: > > The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or > 6a17bcddd6c2 (eberlm). > > The failure is

Re: [isabelle-dev] Nonterminating AFP build

There are multiple failures in PMF_OF_List. It looks like the behaviour of simplification has changed concerning the functions ennreal and ereal. Larry > On 12 May 2016, at 11:39, Lawrence Paulson <l...@cam.ac.uk> wrote: > > It has no timeout, sorry, that was my fault. Now set

[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

A relevant past message. Larry > Begin forwarded message: > > From: Makarius > Subject: Re: [isabelle] TERM exception in fologic.ML > Date: 27 October 2014 at 20:22:02 GMT > To: Slawomir Kolodynski > Cc: "cl-isabelle-us...@lists.cam.ac.uk"

[isabelle-dev] Fwd: [isabelle] TERM exception in fologic.ML

I wonder if we can look at this problem, which has been around for at least 18 months. It seems to be connected with the recent modification to hyp_subst_tac, which now retains the equality. (The workaround of switching off this behaviour is not a true solution.) I took a look at this code

[isabelle-dev] pretty-printing of DIM('a)

The DIM('a) notation is introduced in Multivariate_Analysis/Euclidean_Space, for referring to the dimension of the Euclidean space designated by type ‘a. (See code snippet below.) Unfortunately, DIM(‘a) pretty-prints as card Basis, and the type reference is lost. We need to fix this somehow.

Re: [isabelle-dev] NEWS:

This is a great achievement! And disk space is still important, especially on modern devices with SSDs. My machine has only 20 GB to spare. Larry > On 16 Mar 2016, at 22:33, Makarius wrote: > > *** System *** > > * Poly/ML heaps now follow the hierarchy of sessions, and

Re: [isabelle-dev] Syntax for lattice operations?

What would be the objective of this change? Larry > On 10 Mar 2016, at 10:00, Florian Haftmann > wrote: > > Hi all, > > traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been > kept in a separate library theory, to allow

Re: [isabelle-dev] Preferred syntax for big GCD?

I’m sympathetic to this view. On the other hand, GCD is the only one of these uppercase formulations that’s actually in widespread use. Larry > On 10 Mar 2016, at 09:46, Florian Haftmann > wrote: > > Since there is no generally accepted symbolic

Re: [isabelle-dev] NEWS: HOL notation

We might also consider the negations of \in, \subseteq, \subset and even perhaps < and > Larry > On 5 Mar 2016, at 22:19, Makarius wrote: > > * New abbreviations for negated existence (but not bounded existence): > > ∄x. P x ≡ ¬ (∃x. P x) > ∄!x. P x ≡ ¬ (∃!x. P x)

Re: [isabelle-dev] Notation for not-exists

Agree Larry > On 4 Mar 2016, at 11:34, Makarius wrote: > > I can't imagine anybody using that print mode seriously, so maybe it is time > to make these syntax variants input-only, as a preparation for removal at a > later point.

Re: [isabelle-dev] Nonstandard Analysis

Sure. Or maybe HOL-GCHQ? :-) Larry > On 26 Feb 2016, at 12:30, Makarius wrote: > > The session HOL-NSA contains interesting material that deserves better > visibility. > > How about renaming it to HOL-Nonstandard_Analysis, in analogy to > HOL-Multivariate_Analysis?

[isabelle-dev] NEWS

More complex analysis including Cauchy's inequality, Liouville theorem, open mapping theorem, maximum modulus principle, Schwarz Lemma. (See theory Conformal_Mappings.) Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] [Isabelle-ci] Build failed in Jenkins: afp-repo-checkin #80

I hope I didn’t sound too critical. It’s a very impressive system, but I was anxious to get those problems fixed quickly. I see that somebody else got there first. (I frequently find theorems that are near-duplicates, which I eliminate, and generally I’m pretty good at locating all uses of the

[isabelle-dev] Fwd: [Isabelle-ci] Build failed in Jenkins: afp-repo-checkin #80

Forgive me if I’m overlooking something obvious, but the attached message about a failure in the AFP doesn’t seem to include any clue as to which of the 200+ entries actually failed. I spent a little time poking around https://ci.isabelle.systems/jenkins/ without learning anything more. Is

Re: [isabelle-dev] Supported Poly/ML versions

A pity that even this one is necessary. Has tracing somehow got worse since then, and can’t that be reversed? Larry > On 13 Feb 2016, at 13:42, Makarius wrote: > > * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a >detailed exception trace. Note that

Re: [isabelle-dev] SML/NJ

I don't see the point of continuing with SML/NJ any longer. Larry > On 13 Feb 2016, at 12:07, Makarius wrote: > > Are there remaining uses of SML/NJ, or can it be discontinued now? ___ isabelle-dev mailing list

Re: [isabelle-dev] Grouping ISABELLE_FULL_TEST?

Maybe it’s time. They’ve not made it better, and it seems pretty hopeless now. Larry > On 31 Jan 2016, at 13:41, Makarius wrote: > > We could discontinue ML_SYSTEM_POLYML and merely test the "HOL" session for > SML/NJ. > > Or we could discontinue SML/NJ altogether. I

Re: [isabelle-dev] Multicore timings

I do remember. It’s almost a shame how years of work can be executed in minutes. Larry > On 15 Jan 2016, at 19:16, Makarius wrote: > > The sessions from Bali to JinjaThreads are historically related; this used to > be the top-end in resource usage until 1-2 years ago.

[isabelle-dev] next release

I don't expect to contribute anything else before the next release. There are little bits that I could add, but probably I should desist in the name of stability. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] HOL-Codegenerator_Test error

I had a problem like this last year. Unlike a broken proof, they seem almost impossible to fix. Something’s fragile about this setup. Larry > On 12 Jan 2016, at 11:04, Manuel Eberl wrote: > > There are actually several affected functions: > > Discrete.sqrt > size_fset >

[isabelle-dev] HOL-Codegenerator_Test error

I have finally installed my great mass of new material, but when I try to test it, it fails as shown below. I can’t imagine what I could have done to trigger such an error. Nearly all of my changes are confined to Multivariate_Analysis. Does anybody have an idea what could be going on here?

Re: [isabelle-dev] Towards the release

I'm still working on a major theorem. It would be nice to include it if possible. However, I have no major changes on the order of the real vs of_nat rationalisation. Larry > On 1 Jan 2016, at 19:24, Makarius wrote: > > Isabelle2016-RC0 is published, but we are still in

Re: [isabelle-dev] find_theorems and type class axioms

Perhaps the question relates to how polymorphism is interpreted in these searches. I’m getting the idea that the search for “dist” and “norm” somehow produces a combination of type classes that doesn’t precisely match the instances in the axiom “dist_norm”, where they are too specific to be

Re: [isabelle-dev] Build problems in AFP

I fixed these about two hours ago. Larry > On 3 Dec 2015, at 14:56, Florian Haftmann > wrote: > > isabelle: e1e6bb36b27a tip > afp: be89f13e81c1 tip > >> Running Pratt_Certificate ... >> Running Codegen ... >> Running Sturm_Tarski ... >> Running

Re: [isabelle-dev] MIR decision procedure

We now have presburger as a stand-alone proof method. Possibly the other procedures could be bundled into that. There are times when it is definitely worth the wait. Larry > On 1 Dec 2015, at 16:14, Amine Chaieb wrote: > > At the time we decided against it due to the

Re: [isabelle-dev] Infinite_Set.thy

I have just checked, and this function is used nowhere in our libraries, including the AFP. Larry > On 27 Nov 2015, at 15:59, Tobias Nipkow wrote: > > I remember other people suggesting this as well, albeit not on this list. It > seems fair to me. Only the function

[isabelle-dev] Infinite_Set.thy

This theory proves a number of useful properties of infinite sets, and consequently, of finite sets. I’m wondering whether it makes sense to have this theory (a 17 KB file) in the Library when our main theory Finite_Set.thy (60 KB) is part of the standard HOL development. Of course we are all

Re: [isabelle-dev] find_theorems and type class axioms

> On 26 Nov 2015, at 11:58, Florian Haftmann > wrote: > > The sort constraints of constants play *no* role for > searching theorems. The sort constraints of terms to be searched *do*, > and in my view this is the desired behaviour: if I formulate a

Re: [isabelle-dev] find_theorems and type class axioms

I still have no idea why find_theorems should refuse to find a theorem containing two named constants, no matter what the sorts say. Are there examples of searches that would deliver crazy results if this constraint were lifted? Larry > On 26 Nov 2015, at 14:41, Johannes Hölzl

Re: [isabelle-dev] find_theorems and type class axioms

I had no idea that sort constraints played any role in the finding of theorems, or why they should play a role. Whatever function they have in a search doesn’t prevent the very similar query dist norm "op=“ from picking up quite a few things. To my mind it’s quite unintuitive and maybe

Re: [isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

I am partly to blame. The changes involving the “real” function caused a lot of disruption. I needed a week to get all of Isabelle/HOL working again, and thought it a more practical option to tackle the AFP failures after they occurred. Most of them were only out of action for a day. Larry >

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

As I recall, the Library directory get special treatment. But I forget what this special treatment consists of. It might make sense to move this particular entry to Library. Larry > On 19 Nov 2015, at 09:46, Florian Haftmann > wrote: > > Hi all, >

[isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

These suggestions are worth a discussion. Should we go ahead? Would anybody like to apply this patch and test that everything still works? Larry > Begin forwarded message: > > From: Peter Gammie > Date: 15 November 2015 at 15:15:48 GMT > To:

Re: [isabelle-dev] extra lemmas

These look useful, thanks! I’ll take care of it. Larry Paulson > On 16 Nov 2015, at 16:26, Peter Gammie wrote: > > Can someone add these in at the obvious places? > > thanks, > peter > > lemma LeastI2_wellorder_ex: > assumes "\x::'a::wellorder. P x" > and "\a. \ P a; \b.

[isabelle-dev] find_theorems and type class axioms

Andreas’s message reminds me that axioms of type classes are still not picked up: class dist_norm = dist + norm + minus + assumes dist_norm: "dist x y = norm (x - y)” This item has the status of a theorem. However, the query dist "norm(_-_)” doesn’t find it. Surely it should? Larry

Re: [isabelle-dev] CGSCreateKeyboardEvent

My impression is that this message appears after quitting Isabelle under unusual circumstances, e.g., after it asks you what to do with a modified buffer. I am using OS X El Capitan. Larry > On 15 Nov 2015, at 21:37, Makarius wrote: > > Larry, > > I am forwarding this

[isabelle-dev] MIR decision procedure

The MIR decision procedure is again working. We still have the mystery of what it is good for. It is not used anywhere at all. Even the test suite consists of a mere five problems. And I have now stumbled across ferrack. It seems to be used quite a bit, but what does it do? Is it documented

Re: [isabelle-dev] the function "real"

ook yet into: >> JinjaThreads >> Ordinary_Differential_Equations >> Affine_Arithmetic >> Akra_Bazzi >> >> - Johannes >> >> Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl: >>> Okay, I look at the AFP entries. &g

Re: [isabelle-dev] the function "real"

> > - Johannes > > Am Mittwoch, den 11.11.2015, 18:29 +0100 schrieb Johannes Hölzl: >> Okay, I look at the AFP entries. >> >> I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow >> if this is unusual. >> >> - Johannes >>

Re: [isabelle-dev] the function "real"

There are a great many examples of theorems involving various coercion functions and the relations =, <, <=. In a number of cases, the “real” versions were declared as [iff]-rules, while the “of_nat/of_int” versions were declared as [simp]-rules only. When identifying the two, I decided it

Re: [isabelle-dev] the function "real"

ence > Probabilistic_Noninterference > UpDown_Scheme > Girth_Chromatic > Probabilistic_System_Zoo > Random_Graph_Subgraph_Threshold > pGCL > > Just tell me which of these you are already working on, so we can merge > without conflicts. > > - Johannes > > > Am

Re: [isabelle-dev] the function "real"

> glad to see it gone. > > Thanks for the good work! > > > On 10/11/15 17:45, Lawrence Paulson wrote: >> The first phase of this project is finished: the function “real” now has the >> monomorphic type nat => real and is simply an abbreviation for the generic

[isabelle-dev] the function "real"

The first phase of this project is finished: the function “real” now has the monomorphic type nat => real and is simply an abbreviation for the generic function, of_nat. In addition, the function “real_of_int” abbreviates the generic function of_int. It took about a week to convert all the

[isabelle-dev] real v of_nat

Tomorrow, I hope to start the long-proposed unification of the functions real and of_nat. The plan is to make of these two functions (along with real_of_nat) synonymous. At the moment, real and of_nat are extensionally equal but distinct functions, while real_of_nat is an abbreviation for

Re: [isabelle-dev] NEWS: toplevel theorem statements

This suggestion was mine. Although “proposition” can mean many things, we are talking about mathematical developments. Quite a common convention is to reserve “theorem” for one or two main results, and “lemma” for technical results of no general interest, leaving “proposition” as the main

Re: [isabelle-dev] Problem in the AFP

I've recently pushed some changes affecting the factorial function and simplification of real expressions. Larry Paulson On 21 Mar 2015, at 17:26, Peter Lammich lamm...@in.tum.de wrote: It's the operation identification phase of Autoref, quite difficult to debug ... I have not yet looked

Re: [isabelle-dev] Metis vs. polymorphism

No doubt this is my responsibility, but this very complicated heap of code has been out of my consciousness for many years. Sorting it out would be a non-trivial project. Larry On 30 Dec 2014, at 15:06, Makarius makar...@sketis.net wrote: Metis proof reconstruction is already known to have

Re: [isabelle-dev] Abbreviations and find_theorems

I had no idea that abbreviations ever worked here. Of course it would be nice if they did. Larry On 15 Nov 2014, at 16:58, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: when searching for theorems, abbreviations may behave surprisingly: find_theorems odd _ --

Re: [isabelle-dev] Algebra and number theory in Isabelle/HOL

Your agenda looks impressive but very ambitious. I noticed a remark about the treatment of signs in integer division. You mention two constraints but overlook a third: standard textbooks say that the remainder should have the same sign as the divisor, so that for example -1 mod 2 = 1 and

Re: [isabelle-dev] HOL/Number_Theory/Primes

Surely a dvd b == b mod a = 0” should not be a simple. It can’t be such a difficult change. Larry On 7 Nov 2014, at 17:34, Tobias Nipkow nip...@in.tum.de wrote: Thanks for finding this out. The theorem is a dvd b == b mod a = 0 This applies to any term a mod b and creates a

[isabelle-dev] HOL/Number_Theory/Primes

This theory takes quite a while to load, and I have found out why: text{* A bit of regression testing: *} lemma prime(97::nat) by simp lemma prime(997::nat) by eval The proof that 97 is prime takes 35 seconds on a very fast machine. Can we get rid of this or at least substitute a smaller

Re: [isabelle-dev] NEWS: parameterized antiquotations @{map N}, @{fold N} etc.

I have to admit: although I distinctly remember the name pairself, I can’t imagine what I could have been thinking when I chose this name. Your suggestions make a lot more sense. Larry On 3 Nov 2014, at 09:08, Makarius makar...@sketis.net wrote: On Thu, 30 Oct 2014, Florian Haftmann wrote:

[isabelle-dev] LWP::Simple

I recently tried to launch the Isabelle development version, but got error messages indicating (in a fairly obscure way) the need to install the Perl module LWP::Simple. Something new here? Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] NEWS and INCOMPATIBILITY

I can’t think of any reason to avoid correcting errors of any sort in the NEWS file. Larry On 2 Oct 2014, at 16:55, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: We have a tradition not to change NEWS after release, but maybe we should break this rule and consolidate

Re: [isabelle-dev] Let and tuple case expressions

Agree. Larry On 2 Oct 2014, at 17:13, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: In short, I have come to the conclusion that let (a, b) = p in t case p of (a, b) = t at the moment being logically distinct, should be one and the same. This is very much

<    1   2   3   4   5   >