Perhaps this should be done uniformly for all single-constructor
datatypes, not just pairs. Any case expression with a single branch
could be printed as a "let".
- Brian
On Thu, Oct 2, 2014 at 9:13 AM, Florian Haftmann
wrote:
> In a private discussion, there had been a question what can be done
On Fri, Jul 11, 2014 at 5:54 AM, Askar Safin wrote:
> Hi. I think I found a bug in the Isabelle 2013-2 (OS: Debian GNU/Linux 7,
> Interface: jEdit). For example, I type the following in the jEdit Isabelle
> interface:
>
> ==begin==
> notepad begin
> have "A ==> B" and "C" proof -
> show "A ==>
Hi everyone,
I've noticed that recent changesets (up to 00112abe9b25) on testboard
have completed Pure and HOL tests, but the HOL_makeall results never
show up. (The most recent HOL_makeall report is 3253aaf73a01, dated
March 18.)
Does anyone know why this is? Is one of the HOL theories going int
On Tue, Mar 18, 2014 at 12:55 PM, Makarius wrote:
> Are you actually working together with Johannes Hölzl on these parts, or is
> your later change 32b7eafc5a52 merely a coincidence?
We are not working directly together, but I suppose that the same
email conversation with Larry Paulson has motiva
Revision c7dfd924a165 should now take care of it.
- Brian
On Tue, Mar 18, 2014 at 11:47 AM, Makarius wrote:
> On Tue, 18 Mar 2014, Florian Haftmann wrote:
>
>> hg id 9ffbb4004c81
>
>
> I've noticed this as well, when preparing a push. The broken state means I
> have to roll back and wait until
On Mon, Sep 30, 2013 at 2:34 PM, Makarius wrote:
> According to the normal context discipline, free variables are always fixed,
> like a local const. We have a few tools that violate that principle and
> consequently cause confusion, e.g. the Simplifier. There are sometimes
> historical reasons f
On Fri, Sep 27, 2013 at 12:16 PM, Florian Haftmann
wrote:
>> context field_char_0
>> begin
>>
>> …
>>
>> lemma of_rat_minus: "of_rat (- a) = - of_rat a"
>> apply transfer
>
> the »- _« (name uminus) gets replaced by a bound variable »uminusa«.
> There seems to be a problem with the context here.
23b6/src/HOL/ex/Numeral_Representation.thy
>
> Can we delete that, and keep the history inside the history? Or are there
> remaining aspects that are not in the official numeral implementation (and
> reform) by Brian Huffman?
Numeral_Representation.thy defines a couple of type classe
I discovered a problem with the pretty-printing of some terms (I am
using revision 4392eb046a97).
term "(λ(a, b) (c, d). e) x y"
"case_guard True x
(case_cons (case_abs (λa. case_abs (λb. case_elem (a, b) (λ(c, d). e
case_nil)
y"
:: "'e"
I assume this is a result of the recent chan
if applied to 0 or 2 arguments, and as a case if
applied to 1. I'm not sure it's worth complicating the pretty printer
just to get this behavior back.
- Brian
> On 24.04.2013 02:10, Brian Huffman wrote:
>>
>> I discovered a problem with the pretty-printing of some terms (I
It would be nice to get HOLCF case combinators working with this new
system, as the parsing for HOLCF case expressions has been a bit
broken for some time.
Can case combinators and constructor functions with
continuous-function types be made to work with the "case_tr" (or
"case_translation"?) attr
On Fri, Mar 29, 2013 at 10:40 AM, Joachim Breitner wrote:
> Hi,
>
> Am Freitag, den 29.03.2013, 13:24 +0100 schrieb Makarius:
>> > This has got nothing to do with Isabelle's informal conventions but is
>> > all about the target language's formal rules.
>>
>> The conventions about theory names and
_eq_cancel" on:
>> a + b - 1 = a - 1 + b
>>
>> simp_trace_depth_limit exceeded!
>
>
> These simprocs were introduced by Brian Huffman here:
>
> changeset: 45775:6c340de26a0d
> user:huffman
> date:Wed Dec 07 10:50:30 2011 +0100
> files:
On Tue, Oct 16, 2012 at 1:22 PM, Tjark Weber wrote:
> Class semiring in HOL/Rings.thy [1] assumes
>
> left_distrib: "(a + b) * c = a * c + b * c"
> right_distrib: "a * (b + c) = a * b + a * c"
>
> This is different from the terminology used in Wikipedia [2],
> MathWorld [3] and much of the lit
On Fri, Oct 5, 2012 at 10:37 AM, Makarius wrote:
> On Thu, 4 Oct 2012, Brian Huffman wrote:
>
>> I was reluctant to support "closed" type definitions at all in HOLCF's
>> cpodef and friends, preferring to make (open) the default behavior; but in
>> the end
On Thu, Oct 4, 2012 at 2:17 PM, Makarius wrote:
> On Thu, 4 Oct 2012, Christian Urban wrote:
>
>> "Closed" type definitions with
>>
>> typedef new_type = "some set"
>>
>> are considered legacy. The warning message suggests
>> to use
>>
>> typedef (open) new_type = "some set"
>>
>> but as far as
On Sun, Jul 29, 2012 at 7:11 PM, Makarius wrote:
> The question is if HOL-Plain and HOL-Main still have any purpose. Full HOL
> now takes < 2min on a reasonably fast machine with 4 cores.
Images like HOL-Plain or HOL-Main are often useful when I am doing
development on libraries within the HOL i
On Thu, Jul 19, 2012 at 8:32 AM, Christian Sternagel
wrote:
> I created a repository at
>
> http://sourceforge.net/p/holcf-prelude/
Thanks for setting this up!
> PPS: As I mentioned in an earlier mail. I would like to add a constant "set
> :: 'a Data_List.list => 'a set" for specification purpos
On Wed, Jul 18, 2012 at 8:52 AM, Christian Sternagel
wrote:
> On 07/17/2012 07:53 PM, Brian Huffman wrote:
>> HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
>> nat and int, so you can write types like "nat -> 'a list" or
>> "na
On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
wrote:
> Dear all,
>
> I put together some functions on lists (that I use in some small proof) in
> Data_List.thy. While doing so and thinking about functions and proofs I
> would need in the future, I stumbled across the following points:
>
>
On Thu, May 31, 2012 at 1:36 PM, Makarius wrote:
> On Thu, 31 May 2012, Andreas Lochbihler wrote:
>
>>> At some point, when I have bundles ready to work with the existing
>>> notation commands, we can fine-tune this scheme further, to allow users
>>> to
>>> 'include' syntax in local situations.
>>
Hi Gerwin,
I'm responding also to the development list.
On Wed, May 30, 2012 at 3:36 AM, Gerwin Klein wrote:
> Hi Brian,
>
> not sure if this has anything to do with your change in numerals, but the
> following used to work as expected in Isabelle2011-1:
>
> type_synonym word_length8 = 8
> type
On Tue, May 15, 2012 at 8:18 AM, Tobias Nipkow wrote:
> How can I see the possible cases in an induction, i.e. Show me cases in PG?
You can type the command "print_cases" into your theory file (this
also works in PG).
But then the real question is, how do we expect new users to discover
this fea
On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
wrote:
> is it really the case that currently the only way to obtain ASCII output
> using print modes is by specifying the empty string, like
>
> thm ("") conjE
>
> or did I miss anything? Since this print mode is occasionally useful, I
> suggest
On Sat, Apr 28, 2012 at 9:48 AM, Florian Haftmann
wrote:
> Hi Christian,
>
>> I spotted this strange line in the NEWS (linked from the test website)
>>
>> symp_def ~> (dropped, use symp_def and sym_def instead)
>
> the LHS is before, the RHS is after the change. In particular, the
> symp_def fr
On Sun, Apr 15, 2012 at 3:00 PM, Makarius wrote:
> * Bundled declarations associate attributed fact expressions with a
> given name in the context. These may be later included in other
> contexts. This allows to manage context extensions casually, without
> the logical dependencies of locales an
On Thu, Apr 19, 2012 at 4:02 PM, Makarius wrote:
> On Tue, 10 Apr 2012, Brian Huffman wrote:
>
>> On Tue, Apr 10, 2012 at 3:06 PM, Makarius wrote:
>>>
>>> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
>>>
>>> *** No code
On Sun, Apr 15, 2012 at 2:54 PM, Makarius wrote:
> * Auxiliary contexts indicate block structure for specifications with
> additional parameters and assumptions. Such unnamed contexts may be
> nested within other targets, like 'theory', 'locale', 'class',
> 'instantiation' etc. Results from the
On Tue, Apr 10, 2012 at 3:06 PM, Makarius wrote:
> Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
>
> *** No code equations for one_word_inst.one_word
> *** At command "by" (line 174 of
> "afp-devel/thys/JinjaThreads/Common/BinOp.thy")
>
> What needs to be done here?
This
On Thu, Mar 29, 2012 at 7:50 AM, Florian Haftmann
wrote:
> As it is now, theory »Code_Nat« is
> not announced that prominently, but this is not that critical.
We should at least put an announcement in NEWS about Code_Nat.
However, you have talked about making the binary representation for
"nat"
On Wed, Mar 28, 2012 at 9:15 PM, Florian Haftmann
wrote:
> Btw. for the moment you have not transferred by additional changes
> concerning Efficient_Nat etc. What are your plans for these? To wait
> until the transition proper has fortified a little? Or shall I take
> care for these?
Hi Floria
On Mon, Mar 26, 2012 at 7:23 PM, Makarius wrote:
> On Mon, 26 Mar 2012, Lukas Bulwahn wrote:
>
>> This problem is reproducible on our testboard servers. At the moment, all
>> tests of changesets after 2a1953f0d20d have to be manually aborted because
>> of that reason. I hope you find a solution qu
As of 2a1953f0d20d, Isabelle now has a new representation for binary numerals:
*** HOL ***
* The representation of numerals has changed. We now have a datatype
"num" representing strictly positive binary numerals, along with
functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to
repre
On Sun, Mar 11, 2012 at 12:09 PM, Tobias Nipkow wrote:
> One error in JinjaThreads was fixed, here is the next one:
>
> *** Unknown fact "list_all2_update_cong2" (line 467 of
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
> *** At command "apply" (line 467 of
> "/
Hi Christian,
Please see this thread from isabelle-dev, November 2009:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-November/000713.html
To summarize: A theorem meta_ext (like ext but using meta-equality
"==" instead of "=") is derivable using only theorem operations
On Wed, Feb 15, 2012 at 5:18 PM, Makarius wrote:
> We should probably also explain more explicitly the purpose of
> isabelle-users vs. isabelle-dev. Especially prevent the misconception that
> "users = Isabelle/Isar" and "dev = Isabelle/ML", which was never intended
> that way as far as I am conc
Hello all,
I am writing about the following recent changeset, which adds another
left-fold operator to HOL/List.thy.
author haftmann
Fri Jan 06 10:19:49 2012 +0100 (6 days ago)
changeset 46133 d9fe85d3d2cd
parent 461325a29dbf4c155
child 46134 4b9d4659228a
incorporated canonical f
On Mon, Jan 9, 2012 at 4:04 PM, Makarius wrote:
> Does the old src/HOLCF/IsaMakefile still have any purpose?
It is there so I can type "isabelle make all" in the HOLCF directory
to rebuild just those theories that depend on HOLCF, just as I could
before HOLCF was moved into src/HOL :)
I wouldn't
Hi all,
I have been working on a new numeral representation for Isabelle
recently, and I would like to share it with everyone. An overview of
the design is now available on the Isanotes wiki [1]; a patched
version of the Isabelle hg repo is also available [2].
[1] https://isabelle.in.tum.de/isano
On Sun, Nov 20, 2011 at 9:52 PM, Makarius wrote:
> * Commands 'lemmas' and 'theorems' allow local variables using 'for'
> declaration, and results are standardized before being stored. Thus
> old-style "standard" after instantiation or composition of facts
> becomes obsolete. Minor INCOMPATIBILI
On Fri, Nov 4, 2011 at 8:32 PM, Makarius wrote:
> This syntax is only defined for single abstractions, but the categories got
> mixed up (the nonterminals via syntax types):
>
> syntax
> "_lebesgue_integral" :: "'a => ('a => real) => ('a, 'b)
> measure_space_scheme => real"
> ("\ _. _ \_" [60,
Hello all,
Lately I have been trying to clean up the code of the cancellation
simprocs, and I have come across something I don't understand.
One set of simprocs will cancel factors from inequalities, rewriting
terms like "x * z < y * z" to either "x < y" or "y < x", depending on
whether it can pr
On Wed, Oct 12, 2011 at 4:01 PM, Makarius wrote:
> On Wed, 12 Oct 2011, Brian Huffman wrote:
>
>> After implementing the warning, I dug through the revision history and
>> was surprised to find that my "new" feature actually used to exist! It
>> was r
Hello all,
This is a follow-up to the conversation on the isabelle-users list
from a few months ago, about confusion that arises when using mutual
induction with the "arbitrary" option.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-June/msg1.html
At the time I suggested that their
On Thu, Sep 22, 2011 at 11:34 AM, Alexander Krauss wrote:
> For mere renamings or simple generalizations, we should just go ahead,
> making sure that the conversion table is in the NEWS. Having an extra legacy
> phase here only creates extra work with no benefit for anyone. With a new
> release, p
On Thu, Sep 22, 2011 at 6:10 AM, Makarius wrote:
> On Thu, 22 Sep 2011, Lukas Bulwahn wrote:
>
>> On 09/22/2011 11:36 AM, Peter Lammich wrote:
>
> Perhaps we should start using a standardized process for phasing out
> legacy theorems, like moving them into a separate theory file
>
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban wrote:
>
> Hi All,
>
> Somebody recently added in the NEWS the entry
>
> Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
> INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
> INTER_eq_Inter_image, Inter_def,
On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein wrote:
> After not running in the test for quite some time, JinjaThreads now comes
> back failing:
>
> *** Undeclared constant: "semilattice_sup_class.sup"
> *** At command "definition" (line 20 of
> "/home/kleing/afp/devel/thys/JinjaThreads/Execute/
On Fri, Sep 16, 2011 at 2:01 PM, Florian Haftmann
wrote:
> Hi Brian,
>
> I am not totally happy with changes like:
>
> http://isabelle.in.tum.de/reports/Isabelle/rev/4657b4c11138#l1.7
>
> The proof text itself is shorter than before, but in less trivial
> examples it produces head ache to instanti
On Thu, Sep 15, 2011 at 7:34 AM, Lars Noschinski wrote:
> Hi everyone,
>
> in the following snippet, applying the simplifier causes an error:
>
> --
> theory Scratch
> imports Complex_Main
> begin
>
> lemma
> shows "(3 / 2) * ln n = ((6 * k * ln n) / n) *
On Sun, Sep 11, 2011 at 1:01 PM, Makarius wrote:
> My impression is that NEWS and CONTRIBUTORS for the coming release is still
> somewhat incomplete.
>
> NEWS is not just for bad news -- infamous INCOMPATIBILITY entries -- but for
> any "user-relevant changes". If things are not user-relevant the
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp wrote:
> Formerly the non-emptiness proof was global, now its local!
>
> locale bla =
> assume "False"
> typedef empty = {}
>
> Now I have to put up with the fact the semantic interpretation of empty is
> the empty set. Formerly only non-empty set
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
wrote:
> HOL-Probability FAILED
This is now fixed in the main repo; the following changeset should be
merged back into isabelle_set:
http://isabelle.in.tum.de/repos/isabelle/rev/c10485a6a7af
___
isabell
On Fri, Aug 26, 2011 at 2:02 PM, Andreas Schropp wrote:
>
> So you suggest using e.g.
> if EX x. x : A then A
> else {0}
> instead of A as the semantic interpretation?
> Interesting!
Yes, this is exactly the kind of thing I meant. You could use any
nonempty set you want in place of {0}, of cour
On Fri, Aug 26, 2011 at 1:34 PM, Andreas Schropp wrote:
> locale bla =
> assume "False"
> typedef empty = {}
>
> Now I have to put up with the fact the semantic interpretation of empty is
> the empty set. Formerly only non-empty sets were semantic interpretations of
> type constructors. The way
On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp wrote:
> On 08/26/2011 10:38 PM, Makarius wrote:
>>
>> What is gained from that apart from having two versions of typedef?
>
> I am with you here.
> We don't need two primitive versions of typedefs.
This is incorrect: Only the predicate-based typed
On Fri, Aug 26, 2011 at 1:38 PM, Makarius wrote:
> On Fri, 26 Aug 2011, Brian Huffman wrote:
>
>> Here's one possible approach to the set-axiomatization/typedef issue:
>>
>> As a new primitive, we could have something like a "pred_typedef"
>> operati
On Thu, Aug 25, 2011 at 1:45 PM, Florian Haftmann
wrote:
> HOL-Hoare_Parallel FAILED
> Also Hoare_Parallel is non-terminating.
I have a patch for this one:
http://isabelle.in.tum.de/repos/isabelle/rev/5e681762d538
Once this changeset gets merged into the isabelle_set repo,
Hoare_Parallel shoul
On Fri, Aug 26, 2011 at 9:43 AM, Andreas Schropp wrote:
> On 08/26/2011 07:02 PM, Brian Huffman wrote:
>>
>> I didn't suggest the idea merely for your benefit. I think this
>> approach would give Isabelle a nicer, simpler logical foundation.
>>
>>
>
>
On Fri, Aug 26, 2011 at 9:36 AM, Andreas Schropp wrote:
> On 08/26/2011 06:50 PM, Tobias Nipkow wrote:
>>
>> I agree. Since predicates are primitive, starting from them is
>> appropriate.
>>
>> Tobias
>
> Did I get this right:
> the idea is to implement our advanced typedef via a HOL4-style predi
On Fri, Aug 26, 2011 at 9:20 AM, Andreas Schropp wrote:
> On 08/26/2011 06:33 PM, Brian Huffman wrote:
>>
>> This approach would let us avoid having to axiomatize the 'a set type.
>>
>
> Thanks for trying to help me, but as I said:
> axiomatized set is just a
Here's one possible approach to the set-axiomatization/typedef issue:
As a new primitive, we could have something like a "pred_typedef"
operation that uses predicates. This would work just like the
new_type_definition facility of HOL4, etc.
The type "'a set" could be introduced definitionally usi
On Fri, Aug 26, 2011 at 7:06 AM, Lawrence Paulson wrote:
> I am trying to process the following declaration in Probability/Sigma_Algebra:
>
> inductive_set
> smallest_ccdi_sets :: "('a, 'b) algebra_scheme \ 'a set set"
> .
> .
> .
> monos Pow_mono
>
> I get the following error message (for t
Hello everyone,
Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle
would print a similar warning whenever a definition reuses a name that
is already in scope in the current context. For example, if a theory
defines a c
On Mon, Aug 22, 2011 at 8:01 AM, Lawrence Paulson wrote:
> I've come across something strange in the file
> isabelle/afp/devel/thys/DataRefinementIBP/Diagram.thy and was wondering if
> anybody could think of an explanation.
>
> A proof works only if I insert before it the following:
>
> instance
On Wed, Aug 17, 2011 at 11:51 AM, Florian Haftmann
wrote:
> HOLCF-Library FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/c478cd500dc4
> HOL-Bali FAILED
> HOL-Decision_Procs FAILED
> HOL-Induct FAILED
> HOL-Subst FAILED
> HOL-NanoJava FAILED
Fixed: http://isabelle.in.tum.de/repos/isabe
On Fri, Aug 12, 2011 at 4:07 PM, Makarius wrote:
> http://isabelle.in.tum.de/repos/isabelle/rev/13e297dc improves startup
> time of the worker thread farm significantly, and I've got real times in the
> range of 0.003s -- 0.005s on my "old" machine from 2 years ago with Proof
> General.
Thank
On Thu, Aug 11, 2011 at 5:44 AM, Florian Haftmann
wrote:
> Hi again,
>
> as feasibility study I re-introduced the good old set type constructor
> at a recent revision in the history. The result can be inspected at
>
> http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss wrote:
> What are, actually, the losses when going back? This has not yet been
> touched by this thread at all (except the compatibility/import issue
> mentioned by Brian), and at least myself I wouldn't feel comfortable
> answering this question j
Hello all,
Recently I've been hacking on a bunch of proof scripts using the
development version of Isabelle, and I noticed that when processing
proof scripts, I often get a noticeable pause at uses of "simp_all".
The same pause does not occur with Isabelle2011.
Below is a minimal theory file to d
On Thu, Aug 11, 2011 at 5:43 AM, Florian Haftmann
wrote:
> Hello together,
>
> recently in some personal discussions the matter has arisen whether
> there would be good reason to re-introduce the ancient set type
> constructor. To open the discussion I have carried together some
> arguments. I'm
Your confusion stems from the fact that your theory file is also
called "ms". The "simps" rules generated by the "record" command are
qualified by both the theory name and the type name, so the full names
in your example are "ms.ms.simps" and "ms.aut.simps". Referring to
either of these by their fu
> most
>> cases, instantiations of types (typedefs, records and datatypes) as
>> countable
>> (see ~~/src/HOL/Library/Countable).
>
> It seems that for datatypes we now have such functionality, implemented four
> weeks ago by Brian Huffman:
>
> http://isabelle.in.tum.de
On Sat, Jul 9, 2011 at 10:51 AM, Lukas Bulwahn wrote:
> I think it is reasonable, so I added your changeset and set up the code
> generator and added a simple test case for quickcheck showing that we can
> evaluate floor and ceiling now.
> These preliminary changesets can be inspected under
> http
n 8 Jul 2011, at 02:13, Brian Huffman wrote:
>
>> The drawback to this design is that it requires yet another type
>> class, of which we have plenty already.
>
>
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.
I wrote to Florian about this exact issue back in February 2010.
Florian's recommended solution at the time was to add a new subclass
of archimedean_field that fixes the floor function and assumes a
correctness property about it. This solution is really easy to
implement (see attached diff). If peo
⇒ 'a ⇒ 'b" (binder "Λ " 10)
where "Lambda f ≡ f"
term "λ x. True" (* 'a::{} ⇒ bool *)
term "Λ x. True" (* 'a::type ⇒ bool *)
- Brian
>
> Tobias
>
> Am 29/06/2011 18:12, schrieb Brian Huffman:
>>
>> These
These kinds of situations come up in HOLCF, which declares a default
sort other than "type". Type variables default to being pointed (class
"pcpo" or "domain") but it is often convenient to be able to infer
unpointed types wherever they may occur (class "cpo" or "predomain").
- Brian
On Wed, Jun
Obviously, the naturals assign a non-standard meaning to negative numerals.
But are there any types that assign a non-standard meaning to
*positive* numerals? (By "standard" I mean 2=1+1, 3=1+1+1, 4=1+1+1+1,
etc.) Is there any reason why anyone would ever want to define or use
such a type?
If not
Hello all,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: "nat => nat" where
"foo 0 = 1" | "foo (Suc n) = foo 0"
*** Extra variables on rhs: "foo"
*** The error(s) above occurred in defin
On Tue, Feb 8, 2011 at 9:01 AM, Lawrence Paulson wrote:
> Historically, the point is that index numbers were regarded as very important
> in variable names, while identifiers ending with digits were not seen as
> important. And there are other ways of making multiple identifiers. Nowadays,
> th
The *_tac-style instantiation might be out of fashion, but the same
parsing rules for indexnames are also used with the "where" attribute,
which is still quite useful.
- Brian
On Tue, Feb 8, 2011 at 7:59 AM, Lawrence Paulson wrote:
> Obviously this proposal would involve a significant incompatib
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber wrote:
> On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote:
>> One issue can be that if some sort involves multiple type classes, the
>> corresponding class may not have been defined. That is the one advantage
>> of sorts: you can create conjunctio
Hello all,
I recently discovered that warnings about the secondard search path
are generated more often than they ought to be. I am using repository
version 1fa4725c4656.
Create two files A.thy and B.thy with the following contents:
theory A
imports "~~/src/HOL/Library/Cardinality"
begin
end
th
On Thu, Jan 6, 2011 at 8:59 AM, Makarius wrote:
> If everybody else manages to wrap up until the beginning of next week, we
> have a good chance to release before the end of the month.
This sounds good.
> I think a release date of January 2011 still justifies to call the release
> "Isabelle2010"
On Thu, Dec 2, 2010 at 11:26 AM, Makarius wrote:
> Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about
> an unexpected crash of the typedef package due to hidden polymorphism in the
> set involved, not the type.
It was a simple error message, not a "crash".
> What I did th
On Thu, Dec 2, 2010 at 8:42 AM, Makarius wrote:
> Right now there is already a clear warning -- which Proof General happens to
> show in a hardly visible way, but that is just one of many problems of Proof
> General. In Isabelle/jEdit the warning is hard to miss. I will check again
> about the ot
On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow wrote:
> Is the following behaviour really a good idea and useful?
>
> inductive P :: "nat => bool" where
> "P(suc n)"
>
> is accepted but defines
>
> P :: "'a itself => nat => bool"
>
> It does kind of warn me by saying
>
> ### Additional type variab
On Tue, Nov 30, 2010 at 8:35 AM, Florian Haftmann
wrote:
>>> indeed, both theorems are the same, just with different accesses;
>>> recently, we introduced the concept of mandatory qualifiers to avoid the
>>> strange base accesses (e.g. »induct«, »simps«, »intros«), but this has
>>> never been syst
On Mon, Nov 29, 2010 at 11:47 PM, Florian Haftmann
wrote:
> Hi Sascha,
>
>> There exists a theorem called "induct" in HOL, which changes after
>> every datatype declaration. What is the rationale behind this
>> theorem? Is it required for a particular purpose or just a forgotten
>> remainder of
On Fri, Nov 19, 2010 at 2:40 PM, Joachim Breitner
wrote:
> Hi everyone,
[...]
> I’m sorry for the trouble my submission causes. When writing the
> theories I had planned to actually use the proof document as my project
> report, therefore the trouble I went through to have the syntax as
> similar
! Bad space factor (0).
***
***\let
*** l.27 ...\isaliteral{22}{\isachardoublequoteclose}}
***
{\isaliteral{29}{\isacharp...
***
*** ))
- Brian
> Brian Huffman schrieb:
>> On Fri, Nov 19, 2010 at 7:28 AM, Brian Huffman wrote:
>>> The latex document generation
On Thu, Nov 18, 2010 at 1:58 PM, Makarius wrote:
> For some reason, many people have started to sequeze everything in a single
> line (frequent), or imitate the headline/body text format of other projects
> with a completely different structure (rare). The reason might be as
> profane as the defa
On Thu, Nov 18, 2010 at 2:59 PM, Makarius wrote:
> On Thu, 18 Nov 2010, Brian Huffman wrote:
>
>> The effect of my change "typedef (open) unit" is to remove the
>> definition of the following constant
>>
>> unit_def: "unit == {True}"
>>
&
The effect of my change "typedef (open) unit" is to remove the
definition of the following constant
unit_def: "unit == {True}"
thus making the name "unit" available to users.
- Brian
On Thu, Nov 18, 2010 at 1:58 PM, Makarius wrote:
> Hi Brian,
>
> can you say a few words about b994d855dbd2 jus
ems.sorted_filter(2)
Find_Theorems.find_theorems(5)find_all(2)
Find_Theorems.find_theorems(5)find_all(1)
Find_Theorems.print_theorems(5)
Toplevel.apply_tr(3)(1)
Runtime.debugging(2)(1)
End of trace
*** exception UnequalLengths raised
*** At command "find_theorems"
>
>
> Lar
Hello everyone,
Recently I noticed that in HOLCF, whenever I do a theorem search for
theorems containing the constant "UU" (i.e. bottom), the search fails
with an UnequalLengths exception. I tracked the problem down to this
specific theorem from Fun_Cpo.thy: Before this point, find_theorems
"UU" s
On Fri, Nov 12, 2010 at 5:48 AM, Makarius wrote:
> On Thu, 11 Nov 2010, Brian Huffman wrote:
>> Here is the reason I am reluctant to use transparent ascription:
>> Programmers use modules and signatures as an abstraction mechanism. (I
>> shouldn't need to explain
Hello everyone,
The recent appearance of some new warning messages got me thinking
about transparent-vs-opaque ascription again. (I.e. "structure Foo :
FOO = struct ... end" vs "structure Foo :> FOO = struct ... end")
http://isabelle.in.tum.de/repos/isabelle/rev/daaa0b236a3f
Here is the reason I
On Wed, Nov 3, 2010 at 8:17 AM, Makarius wrote:
> On Wed, 3 Nov 2010, Brian Huffman wrote:
>> The 'typedef' command supports a similar option for alternative names;
>> I am sure that it was originally created for use with non-alphanumeric
>> type names. One could al
1 - 100 of 191 matches
Mail list logo
