Re: [isabelle-dev] NEWS: activation of Z3 via z3_non_commercial system option

2014-01-15 Thread Makarius
On Mon, 13 Jan 2014, Lawrence Paulson wrote: I get an error here: ~/isabelle/Repos/src/HOL: isabelle components -a ### Missing Isabelle component: /Users/lp15/.isabelle/contrib/z3-3.2-1 Getting http://isabelle.in.tum.de/components/z3-3.2-1.tar.gz; Can't locate LWP/Simple.pm in @INC (@INC

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

2014-01-15 Thread Makarius
On Tue, 14 Jan 2014, Thomas Sewell wrote: This is also a patch against Isabelle2013-1. Is that just a typo, or are you still using that failed release? The current one is Isabelle2013-2, and it does not introduce any incompatibilities over Isabelle2013-1, so there is no reason to keep

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

2014-01-15 Thread Makarius
On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] Larry, you are the original author of hypsubst. Does the hypsubst_thin terminology make sense to you? It is used here both for the

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

2014-01-15 Thread Lawrence Paulson
The name makes sense: thin refers to deleting the assumption. It is ugly of course, which will be an incentive for users to update their proofs. Larry On 15 Jan 2014, at 15:05, Makarius makar...@sketis.net wrote: On Tue, 14 Jan 2014, Thomas Sewell wrote: If there is some collection of

[isabelle-dev] NEWS: newline in HOL char or string literals

2014-01-15 Thread Makarius
* The symbol \newline may be used within char or string literals to represent (Char Nibble0 NibbleA), i.e. ASCII newline. This refers to Isabelle/e33c5bd729ff, which also introduces a unicode glyph for that. It is a continuation of the isabelle-users thread:

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

2014-01-15 Thread Thomas Sewell
Whoops. It's both a typo and use of the wrong release. The patch happens to work against Isabelle2013-1 or Isabelle2013-2, since there are no relevant differences in the theory sources. I can confirm that isabelle build -a works in either 2013-1 or 2013-2. Short version of the story, I