This is just to confirm that the result looks really great on my linux
(Fedora 29 with i3) setup. Thanks!
chris
On 2/10/19 7:47 PM, Makarius wrote:
> On 08/02/2019 10:03, Christian Sternagel wrote:
>>
>> I am glad to hear that others have the same experience, I thought my
>>
Dear all,
I am glad to hear that others have the same experience, I thought my
eyes were going bad ;)
But seriously, "buy a new screen" is not always possible. For example,
in the upcoming summer term I am teaching an Isabelle class at the
University of Innsbruck. In my experience (and I just
On 10/08/2018 04:14 PM, Makarius wrote:
> On 08/10/18 15:58, Lars Hupel wrote:
>
> I don't mind if it is possible to eliminate AFP/HLDE (theory
> Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from
> doing such things in AFP.
>
Compiling a binary in HLDE was a mere experiment
On 10/05/2018 10:14 PM, Makarius wrote:
>
> So the question is reduced by one step: What is the purpose of theory
> "Solver_Code" abstractly?
I just wanted to confirm that the purpose of Solve_Code is to produce a
Haskell executable (that implements an algorithm that was formalized in
the AFP
Dear Makarius
On 10/05/2018 07:10 PM, Makarius wrote:
> What is the purpose of the session HLDE, with its duplicate theory
> Solver_Code that is also in Diophantine_Eqns_Lin_Hom?
As the author of the corresponding ROOT file, when I look at it now, I
cannot think of any reason to have also
Just for the record: Makarius' reply resolved the issue for me (see also
below).
On 05/09/2018 11:57 PM, Makarius wrote:
> On 26/03/18 13:48, Christian Sternagel wrote:
>>
>> Thanks, I forgot about that option.
>>
>> With "isabelle latex" in the spe
n.
Type H for immediate help.
...
Should isabelle-eps-converted-to.pdf exist on my system?
cheers
chris
On 03/26/2018 01:26 PM, Makarius wrote:
> On 26/03/18 09:33, Christian Sternagel wrote:
>>
>> I don't see a significant difference in output between my original
>>
>> isabe
em"
I am still unclear on why "isabelle document" fails in both cases.
cheers
chris
PS: Anyway, I can get the manual from the URL you provided. Thanks!
On 03/23/2018 11:51 AM, Makarius wrote:
> On 23/03/18 10:29, Christian Sternagel wrote:
>>
>> Is there a way to ge
Dear Makarius,
I am on 67927:0b70405b3969 and
./bin/isabelle build_doc system
doesn't work for me. I get the error:
Build started for documentation "system"
Cleaning System ...
Running System ...
System FAILED
...
isabelle document -d
Dear list,
maybe the following results about "lex" are worthwhile to add to the
library?
lemma lex_append_right:
"(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
by (force simp: lex_def lexn_conv)
lemma lex_append_left:
"(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex
Dear all,
speaking of "chain", for me the main motivation of introducing "linked
P" was in order to work well together with the corresponding
generalizations of "take_while" and "drop_while", which are called
"take_chain" and "drop_chain" in the AFP entry Efficient-Mergesort.
E.g., "take_chain
On 07/02/2017 10:59 PM, Makarius wrote:
> On 02/07/17 22:16, Christian Sternagel wrote:
>>
>>> It should work analogously to the "Preview" button, but without having a
>>> button.
>>
>> Preview (more concretely the "Open Preview" "
On 07/02/2017 02:21 PM, Makarius wrote:
> On 02/07/17 13:31, Christian Sternagel wrote:
>> On 07/01/2017 09:21 PM, Makarius Wenzel wrote:
>>> There is also a "State" panel that imitates the dockable of the same
>>> name in Isabelle/jEdit. You will get to that
On 07/01/2017 09:21 PM, Makarius Wenzel wrote:
> On 01.07.17 20:46, Christian Sternagel wrote:
>>
>> It only took me some time to find the OUTPUT "panel" (View ~> Output) ;)
>
> That is a plain-text channel of VSCode.
Oh, okay.
>
> There is also a
might be convenient.
cheers
chris
On 05/18/2017 10:34 AM, Makarius wrote:
> On 18/05/17 09:03, Christian Sternagel wrote:
>>
>> I was just about to have a look at the latest and greatest Isabelle (
>> f35abc25d7b1 ) when I noticed the following behavior.
>&g
Dear list,
I was just about to have a look at the latest and greatest Isabelle (
f35abc25d7b1 ) when I noticed the following behavior.
I started with
isabelle jedit -bf
and then tried
isabelle jedit -l HOL
but got an error message about missing files (see PS for details).
Now, these
This email refers to the following commit:
http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251
code abbreviation for mapping over a fixed range
Is there a specific reason for this code equation:
"map_range f (Suc n) = map_range f n @ [f n]"
It seems rather inefficient. Anyway,
Dear all,
http://afp.sourceforge.net/ seems to be down. Just out of curiosity:
Does anyone know for how long and why?
-cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
On 04/17/2015 12:04 AM, Makarius wrote:
On Tue, 7 Apr 2015, Christian Sternagel wrote:
PS: I'm still waiting for
isabelle build -n -a -d '$AFP' -k qualified
to finish (but I guess proper checking, taking semantics into account,
is just expensive). Oops, while writing this email I obtained
Very nice!
I'll wait until the naming issue is settled before replacing my many
uses of hide_const (open)
A further naming suggestion:
(a) private/hidden
(b) qualified
the latter is akin to Haskell's qualified import.
cheers
chris
PS: I'm still waiting for
isabelle build -n -a
Just for the record. I think I experienced something similar:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2015-January/005864.html
cheers
chris
On 03/05/2015 11:39 AM, Johannes Hölzl wrote:
In rev 304ee0a475d1 I fixed a problem that only appears when one loads
(mq) patch
(after testing it of course) ;) ?
cheers
chris
On 01/16/2015 02:40 PM, Christian Sternagel wrote:
Here is a related thread
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04950.html
which was originated by myself ;) (how embarassing).
cheers
chris
During a visit of Florian in Innsbruck we had some discussion on adhoc
overloading. One suspicion was that schematic type variables from
variants had to be paramified before using the resulting type unifier.
I tried to do so in the attached patch. Unfortunately, I still obtain
the following
I think the following thread is related to your question:
http://comments.gmane.org/gmane.science.mathematics.logic.isabelle.user/10007
On 01/26/2015 09:30 AM, Florian Haftmann wrote:
I have some doubt whether the parsing of strings by Isabelle/ML conforms
to plain ML.
See the following
As of c7f6f01ede15 I noticed the following behavior. Suppose I have a
theory file with the following content
theory Foo
imports
Main
begin
end
So far so good. Now I add another import.
theory Foo
imports
Main
~~/src/HOL/Tools/Adhoc_Overloading
begin
end
By
Dear all,
in Isabelle2014 as well as c7f6f01ede15 I noticed that the output when
using adhoc overloading together with abbreviations is not optimal
(maybe this was already discovered before but I forgot about it). Now,
it turns out that the same issue (at least superficially it's the same,
style or not)
that somehow drowned in previous emails:
delete
drop_semicolons
cheers
chris
On 12/01/2014 01:56 PM, Christian Sternagel wrote:
Thanks for the valuable pointers Florian!
As far as I understand, type inference is a necessary prerequisite for
expand_abbrevs (so that afterwards
Dear BNF gurus,
is there a reliable way to check - given the name of a type constructor
- how many dead type parameters it has?
I tried
(case BNF_FP_Def_Sugar.fp_sugar_of lthy tname of
SOME sugar =
if BNF_Def.dead_of_bnf (#fp_bnf sugar) 0 then
error ...
...
However
Hi Jasmin,
thanks for the quick reply. Your suggestion works fine!
cheers
chris
On 12/03/2014 03:46 PM, Jasmin Christian Blanchette wrote:
Hi Chris,
is there a reliable way to check - given the name of a type constructor - how
many dead type parameters it has?
I tried
(case
Dear Makarius,
nowadays I'm doing all my ML coding in Isabelle/PIDE, which is really
nice to use by the way.
A tiny thing I noticed recently is that in the presence of control
symbols, string literals are highlighted somewhat strange. To see what I
mean, consult the attached screenshot,
://isabelle.in.tum.de/testboard/Isabelle/rev/fd70d029af7e
Dmitriy
On 23.11.2014 21:20, Christian Sternagel wrote:
*Moved from isabelle-users*
Thanks for the crucial hint Dmitriy!
Coming back to the original issue of Andreas, some explanation might
be in order.
What we did until now
,
Dmitriy
On 22.11.2014 21:02, Christian Sternagel wrote:
I'm currently a bit confused by the result of Sign.typ_unify (or
rather the result of applying the corresponding unifier). So maybe
the problem stems from my ignorance w.r.t. to its intended result.
After applying the attached debug patch
Dear list,
sorry for the subject ;)
René and I are currently at adapting the Show(_Generator) entry of the
AFP to the new datatype package. And again we stumbled across some
difficulties we already encountered when adapting the Order_Generator
(and which are not resolved yet).
I think it
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type parameters. (As I understand it, this was done just a
Hi Florian,
many month ago I was also surprised, then annoyed, and then I got used
to always adding the underscore-argument.
I fully agree that users shouldn't have to worry about such technicalities.
cheers
chris
On 11/15/2014 05:58 PM, Florian Haftmann wrote:
Hi all,
when searching for
(moved from isabelle-users since I'm referring to the development
versions of Isabelle and the AFP below)
Dear Julian,
unexpectedly I found some time to have a look earlier.
First, the naming layer provided by the lemmas statements in
Prefix_Order is there to keep compatibility with some AFP
moved from isabelle-users
*
Dear all,
In the attached theory files I tried to follow the let Haskell moan if
it is not linear approach. And on first sight it seems to work.
My motivation is to be able to use imperative code inside pure functions
(in the sense that
Dear developers,
the following lemma seems like a basic fact about rtrancl:
lemma rtrancl_map:
assumes ⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s
and (x, y) ∈ r⇧*
shows (f x, f y) ∈ s⇧*
using assms(2, 1)
by (induct) (auto intro: rtrancl.rtrancl_into_rtrancl)
I didn't find it in Main. Did
-Imperative_HOL
as well as
isabelle afp_build Separation_Logic_Imperative_HOL
as far as I can tell the only session in the AFP depending on
Imperative_HOL.
I did not obtain any errors.
cheers
chris
On 09/26/2014 01:00 PM, Christian Sternagel wrote:
Dear Florian,
I will check your proposal. However, I
Dear all,
just an observation. The facts
List.drop_Suc_conv_tl:
?i length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
List.nth_drop':
?i length ?xs ⟹
?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
are duplicates of each other.
cheers
chris
Dear all,
routinely checking IsaFoR against the development version of Isabelle
(more precisely d0dffec0da2b) I stumbled across the following
proof-breaking inconvenience:
In Isabelle2014 and earlier we could do
notepad
begin
fix p :: ('a × 'b × 'c) and xs
assume p ∈ set xs
then
Thanks for your replies!
I forgot to check the NEWS ;)
For the record: the change affected in the order of 10 proofs in IsaFoR
(most of which unnecessarily chained facts into the cases method) which
where of course trivially repaired.
cheers
chris
On 09/05/2014 02:48 PM, Jasmin Christian
Thanks! I'll take care of the AFP now. -cheers chris
On 07/03/2014 02:41 PM, Florian Haftmann wrote:
Hi Christian,
see now
http://isabelle.in.tum.de/repos/isabelle/rev/b69a1272cb04
Cheers,
Florian
On 30.06.2014 15:59, Christian Sternagel wrote:
Dear developers,
would
Christian Sternagel patch-file
In the AFP the attached changes do only influence my entry
Well-Quasi-Orders and (to a tiny amount) Myhill-Nerode, for which I have
corresponding patches in my local AFP repo.
The intention behind the patches is as follows:
* No built-in reflexivity for list
Dear all,
how about adding the following lemmas to the order class?
lemma (in order) rtranclp_less_eq [simp]:
(op ≤)⇧*⇧* = op ≤
by (intro ext) (auto elim: rtranclp_induct)
lemma (in order) tranclp_less [simp]:
(op )⇧+⇧+ = op
by (intro ext) (auto elim: tranclp_induct)
lemma (in order)
On 04/14/2014 12:01 PM, Makarius wrote:
So what are the characteristic points for theory presentation, either
(1) as paginated PDF,
(2) as static HTML,
(3) as dynamic document within the Prover IDE?
I hope I got it right that you are interested in opinions here?
Otherwise, sorry ;)
Dear Lars,
today I first tried using the new simplifier tracing facility (within
Isabelle/jEdit). I just started but have already some questions ;)
In the Simplifier Trace panel itself I did not find out how to get any
output. Only after pressing the Show Trace button a new window opens
Dear all,
recently I was working a lot with adhoc_overloading. Doing so I often
experienced that my output differed from my input (w.r.t. adhoc
overloading). At that time I did not think too much about it since being
able to input readable formulas was quite enough. But today I suddenly
had
Reviving this old thread once more ;)
I think I need some clarifications first:
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
Reviving this old thread, Peter and me found out what is actually going
on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such
Looks good. Sorry for the delay, and for dropping this check in the
first place (honestly I do not remember why I dropped it, but I do
remember that it was no accident ... I guess I was convinced that it
would not do any harm ;)).
chris
On 11/21/2013 10:02 PM, Makarius wrote:
On Thu, 21 Nov
Sorry for the delay (I'm currently moving from Japan back to Austria, and
moving in takes longer than expected... Thus only irregular internet access.)
I'll have a look today in the afternoon if that is okay, otherwise I'm sure
that Dmitriy knows what he is doing :-)
cheers
chris
Makarius
Maybe this thread is of interest
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03773.html
(It contains an overview.html that I once started but never finished.)
cheers
chris
On 09/30/2013 08:28 PM, Lawrence Paulson wrote:
Early in 2013 I was planning to
On 09/30/2013 07:33 PM, Makarius wrote:
On Tue, 24 Sep 2013, Christian Sternagel wrote:
After this changeset, variants may be arbitrary terms (due to
localization). Now replacing a variant by the corresponding overloaded
constant is done by rewriting (as Florian already pointed out
Thanks Jasmin!
@Peter: Does this patch work with your developments as expected?
cheers
chris
On 09/30/2013 10:18 PM, Jasmin Christian Blanchette wrote:
Am 30.09.2013 um 15:07 schrieb Christian Sternagel c.sterna...@gmail.com:
It seems that the required changes are minimal. See the attached
Some more details:
until 0d0c20a0a34f we have the expected behavior. With
changeset: 52622:e0ff1625e96d
user:wenzelm
date:Fri Jul 12 16:19:05 2013 +0200
summary: localized and modernized adhoc-overloading (patch by
Christian Sternagel);
term bind (Some my_abbrev) f
My two cents,
Last time I tried, there was no auto completion available in the input of the
find theorem panel. Which makes the variant of typing find_theorems yourself in
the main buffer more convenient for me at the moment.
Also I experienced already several hangs with this panel as well as
On 09/04/2013 02:24 AM, Makarius wrote:
On Tue, 3 Sep 2013, Christian Sternagel wrote:
Just for the record: the above mentioned hand also sometimes happens
when typing V ... E ... R ... Y ... slowly ;). It is just more
frequent when typing faster (mainly because a hang only ever happens
On 09/04/2013 12:16 AM, Makarius wrote:
In parallel to that, you can try a different Linux on your hardware,
either just a virtual one, or one that is booted from a USB stick
(Ubuntu supports that nicely).
I did so with an 'Ubuntu 13.04 Raring Ringtail - Release amd64' live
USB stick and was
Same here. - cheers chris
Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote:
Are there clubs of iff vs. non-iff? If almost everybody is a member
of the iff club we could just remove that print mode. (We don't have
to consider that for the coming release, to avoid any
On 09/02/2013 06:30 PM, Makarius wrote:
On Sat, 31 Aug 2013, Christian Sternagel wrote:
First note that for me keyboard input to Isabelle/jEdit typically
hangs every 10 minutes or so, depending on how fast I type (but this
is an old and known issue).
I was hoping that it would have
Dear Makarius,
First note that for me keyboard input to Isabelle/jEdit typically hangs
every 10 minutes or so, depending on how fast I type (but this is an old
and known issue).
In Isabelle2013 the completion popup was not triggered when deleting
characters (with backspace). Now this is the
Just an observation. Assuming that the grayish background highlighting
really indicates prover activity in the background, I recently noticed
that sometimes a re-check of the whole buffer is done in situations
where this is (as far as I see) not necessary. For example, having
lemma ...
Dear Alex and all,
once again I started to transform a rather adhoc parser datatype (in
IsaFoR) into some (I think) nicer variant using abstract datatypes with
invariants. After tinkering around for several days (where everything
worked out nicely) I hit a wall, and also remembered that I
is not consuming, but cp = f is).
Concerning readability it would be neat if I could overload bind for
all these cases.
Any comments?
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376987651 -32400
# Tue Aug 20 17:34:11 2013 +0900
# Node ID
all such references to theorem-names accordingly.)
cheers
chris
# HG changeset patch
# User Christian Sternagel
# Date 1376718288 -32400
# Sat Aug 17 14:44:48 2013 +0900
# Node ID be89d558ec26179cdd6da4629492ecca50c4829f
# Parent cba2ddfb30c47192ecfbb531494a423125a1bb8b
more document
Dear all,
currently it is possible to write something like \ , \\, `\``, or
`\\` (i.e., there are escape sequences for the delimiters of strings and
altstrings, as well as for backslash).
What many people might be used to from programming languages does not
work however, e.g., \n, \t, ...
of my laptops fan).
By setting unify_trace_bound to the same value for which
unify_search_bound succeeded, everything was fine again.
Sorry for the false alarm.
cheers
chris
On 08/06/2013 02:40 PM, Christian Sternagel wrote:
Dear all,
I'm currently checking IsaFoR [1] against the repository
attached a file containing all my changes.
cheers
chris
On 08/06/2013 03:34 AM, Makarius wrote:
On Fri, 2 Aug 2013, Christian Sternagel wrote:
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite
On 08/02/2013 12:04 AM, Makarius wrote:
On Wed, 17 Jul 2013, Christian Sternagel wrote:
in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of
such useful tools.
Do you feel like making an example theory, e.g.
src/HOL
are welcome.
cheers
chris
On 07/11/2013 04:36 PM, Christian Sternagel wrote:
Dear all,
here is an update to my previous message. Corresponding patches are
attached (tested with `isabelle build_doc -pa` and `isabelle afp_build
-A`).
Some comments:
1) Variants are stored as terms but where all types
;)).
cheers
chris
On 07/12/2013 08:38 PM, Makarius wrote:
On Fri, 12 Jul 2013, Makarius wrote:
On Fri, 12 Jul 2013, Christian Sternagel wrote:
Dear all,
please find attached patches for localizing
src/Tools/Adhoc_Overloading.thy.
I will take care to apply the changesets to Isabelle and AFP
Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?
My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type
a :: 'a
begin
ML {*
val T1 = @{term a} | singleton (Variable.polymorphic @{context}) |
fastype_of
val T2 = @{term a} | (fastype_of # Term.map_type_tfree (TVar o
apfst (rpair 0)))
*}
end
Dmitriy
Am 11.07.2013 09:01, schrieb Christian Sternagel:
Dear Dimitriy,
thanks that does the trick
/2013 04:38 PM, Christian Sternagel wrote:
First of all, thanks for all the useful answers and sorry for my late
reply (I visited a conference and had some holidays ;)). As Alexander
suggested, I first tried to modify the existing adhoc_overloading.ML in
such a way that variants may be arbitrary terms
. It is for hardcore
kernel operations only
So should I manually check the result for equality, or does the
framework do this for me?
Alex
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match for that
matter)?
My question arises as follows. In adhoc_overloading.ML previously
Sign.the_const_type was used to obtain the type of a constant.
Dear all,
I find myself considering the following cases every now and then:
1) If we know that some property P is true for infinitely many elements
of a well-ordered set (all my use-cases so far, just concern natural
numbers) it is in principle trivial to enumerate them in increasing
order.
, something is
going wrong there.
Cheers,
Gerwin
On 06/06/2013, at 1:48 PM, Christian Sternagel
c.sterna...@gmail.com wrote:
Btw: the links do not seem to work anyway. But why not replace them
with working links instead of just dropping them?
On 06/06/2013 12:40 PM, Christian Sternagel wrote
Dear all,
to update the change history of one of my AFP entries, I ran
admin/sitegen. I noticed that as a result some other sites changed too.
All the changes where along the lines of
-(revision a
href=http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/f74a8be156a7;f74a8be156a7/a)br
Btw: the links do not seem to work anyway. But why not replace them with
working links instead of just dropping them?
On 06/06/2013 12:40 PM, Christian Sternagel wrote:
Dear all,
to update the change history of one of my AFP entries, I ran
admin/sitegen. I noticed that as a result some other
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature
Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor.
Dear all,
I think a similar mail was sent a while ago (but I do not remember by
whom and also was unable to excavate it):
1) In code completion the order of suggestions is sometimes odd
(meaning that a different order would make the usual work-flow
smoother). E.g., when I start with find I
Dear Florian,
I just confirmed that I get the same error message for my default
afp-devel clone (i.e., it used to work with
afp.hg.sourceforge.net/hgroot/afp/afp).
cheers
chris
On 03/23/2013 07:01 PM, Florian Haftmann wrote:
cf. doc/maintenance.html:
Check out the archive from the
-orders
To: Christian Sternagel c.sterna...@gmail.com
Cc: isabelle-dev
isabelle-dev@mailbroy.informatik.tu-muenchen.de, Andrei Popescu
uuo...@yahoo.com
Date: Thursday, February 28, 2013, 4:04 PM
I'm all in favour of refactoring the proofs. That might occasion
moving
. It isn't
especially large. Such a change really has nothing to do with the question of
locating proved results, and it would make it harder to examine past versions.
Larry
On 27 Feb 2013, at 05:57, Christian Sternagel c.sterna...@gmail.com wrote:
Dear all,
in the meanwhile I had a close look
Dear all,
how about adding Andrei's proof (discussed on isbelle-users) to
HOL/Library (or somewhere else)? I polished the latest version (see
attachment).
cheers
chris
PS: In case you are wondering: Why is he interested in these results?
Here is my original motivation: In term rewriting,
On 02/19/2013 03:49 PM, Tobias Nipkow wrote:
Am 19/02/2013 03:50, schrieb Christian Sternagel:
I'm not sure how much work it would be to use this new definition of
reflexivity. But if people think that what I say makes sense (or is more natural
as reflexivity), I would give it a try and report
it
is worth.
Larry
On 18 Feb 2013, at 05:45, Christian Sternagel c.sterna...@gmail.com wrote:
Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant Isabelle/HOL
theories),
already several times I stumbled upon the definition of Relation.refl_on (and
thus also Order_Relation.Refl
Dear Larry, Stefan, Tobias, and Andrei (as authors of the relevant
Isabelle/HOL theories),
already several times I stumbled upon the definition of Relation.refl_on
(and thus also Order_Relation.Refl) and was irritated.
What is the reason for demanding r = A * A? And why are other
properties
:
On Fri, 25 Jan 2013, Christian Sternagel wrote:
It might be good to consolidate your main points in a much shorter webpage.
Your paper is structured (naturally) as a paper, but for the corresponding
webpage I would delete the abstract and most of the introductory material. I
wouldn't actually
I just noticed that the first few lines of the text on index.html and
overview.html are identical. That's a bit odd.
cheers
chris
On 02/15/2013 03:27 PM, Christian Sternagel wrote:
Here is what I came up with. I merged it with the text of the existing
overview.html (from there I just dropped
Just as a further data point: when visiting
http://isabelle.in.tum.de/website-Isabelle2013-RC2/dist/Isabelle2013-RC2/CONTRIBUTORS
using firefox (on Linux) where the default encoding on the client side
is Western ISO-8859-1 then some symbols are strange.
If I explicitly set the encoding to
Dear Gerwin,
Its already a bit late for my idea and maybe I'm the only one in that
situation, but at least for me it would make sense to wait with the AFP
release until the paper submission deadline of ITP. (Since the dates are
rather close anyway and ITP submissions should be accompanied by
target of any README file.
cheers
chris
Larry
On 23 Jan 2013, at 00:19, Christian Sternagel c.sterna...@gmail.com wrote:
I tried to summarize most of the issues that made it to the Isabelle mailing
lists (at that time) in my submission to the Isabelle Users Workshop.
http://arxiv.org
I tried to summarize most of the issues that made it to the Isabelle
mailing lists (at that time) in my submission to the Isabelle Users
Workshop.
http://arxiv.org/abs/1208.1368
It's definitely incomplete, but maybe it could help.
cheers
chris
On 01/23/2013 04:07 AM, Tobias Nipkow wrote:
this
patch to send it to the isabelle-dev mailing list -- via 'hg bundle'
or in some other way?
Thanks!
On 12/28/12 5:10 AM, Christian Sternagel wrote:
Dear Alessandro,
the necessary steps are outlined in the community wiki, here
https://isabelle.in.tum.de/community
Dear Alessandro,
the necessary steps are outlined in the community wiki, here
https://isabelle.in.tum.de/community/Publish_contributions_as_an_external
Since the status of the wiki is not clear at the moment. I summarize the
steps also in this e-mail for later reference.
0) confirm with
Dear all,
just now, when I tried
hg in
in the development repo, I got the error below. My mercurial version is
2.2.3 (for at least some weeks). Did anybody else experience similar
problems?
cheers
chris
comparing with http://isabelle.in.tum.de/repos/isabelle
searching for changes
Dear all,
I think I already used the $AFP in my original submission. The reason
was that having such a variable seemed more robust to me than just
having a relative ../ (so a user could put the entry anywhere he
wants). Sorry for the confusion.
cheers
chris
On 12/14/2012 07:18 PM, Gerwin
1 - 100 of 180 matches
Mail list logo
