Am 02.04.2012 13:36, schrieb Florian Haftmann:
/mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml:
line 77: 27590 Killed $POLY -q $ML_OPTIONS
*** Code check failed for SML: $ISABELLE_PROCESS -r -q -u Pure
*** At command export_code (line 17 of
~~/src/HOL/Codegenerator_Test
I'm indedd quite curious, but unable to build the tex sources. The first
error complains about a missing »eulervm.sty«, with lot of further messages
following.
You mean you couldn't run the tex sources? Unfortunately I can confirm that.
It appears that the tex installation on the macbroys
I'm indedd quite curious, but unable to build the tex sources. The
first error complains about a missing »eulervm.sty«, with lot of further
messages following.
Maybe the necessary dependencies can be found out by using a different
machine to build on, e.g. one of the macbroyXY?
Cheers,
Hi Christian,
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an ad-hoc using [to_pred].
You can also prove theorems for pred relations by means of … by (fact …
[to_pred]), as has been done in many
Hi Christian,
by the way, I noticed that sometimes [to_pred] yields undesirable
results (containing case-expressions), e.g.,
thm trancl_power[to_pred]
results in
(case ?p of (x, xa) ⇒ ?R^++ x xa) =
(∃n0. case ?p of (x, xa) ⇒ (?R ^^ n) x xa)
is this an inherent problem or could this
Hi Christian,
To come back to the subject, I'm missing iteration of predicates,
i.e., what _^^n is on relations but for predicates ('a = 'a =
bool).
this has been added in
http://isabelle.in.tum.de/testboard/Isabelle/rev/69cee87927f0 – you can
transfer theorems from the set relations in an
However, you have talked about making the binary representation for
nat the default in HOL-Main, i.e. merging Code_Nat into the Nat/Num
theories. Are you still interested in doing this?
Definitely, among other related things. But I'm not very optimistic
this can be done before the end of
I have
* linked the existing OpenJDK 1.6 on macbroyXYZ to
/home/isabelle/contrib_devel/jdk
* and added one line to the mira default settings to set
ISABELLE_JDK_HOME accordingly
in order to provide and ad-hoc setup for the mira tests.
I have no idea how platform-indepedent this symlink is, so
I guess someone must restart the mira deamons in order to run with the
adjusted configurations.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
Hi all,
Once there has been the idea that everyone having commit access to the
Isabelle master repository (POSIX group isabelle at nfsbroy) is also a
isatest subscriber.
Maybe it would be helpful to establish this as a rule (at least of
thumb). Isatest mails can still be sorted out by local
This is explained by looking at the history: The typedef package
introduces names with underscores, quotient_type and quotient_def
inherit this from typedef.
This is a misunderstanding. The names generated by »typedef« have
always been retained »as they are«, merely for the sacrosanctity of
Hi Jesus,
trying to import simultaneously the theory file
HOL/Matrix/Matrix.thy and the afp entry
http://afp.sourceforge.net/entries/Matrix.shtml into a file, it seems
that the second theory file unloads the first one (as Makarius
suggested in his mail):
theory Matrix_ex
imports
What I had in mind was something as can be found e.g. in
src/HOL/Library/Dlist.thy:
definition empty :: 'a dlist
where
empty = Dlist []
definition insert :: 'a \Rightarrow 'a dlist \Rightarrow 'a dlist
where
insert x dxs = Dlist (List.insert x (list_of_dlist dxs))
definition remove :: 'a
This is explained by looking at the history: The typedef package
introduces names with underscores, quotient_type and quotient_def
inherit this from typedef.
This is a misunderstanding. The names generated by »typedef« have
always been retained »as they are«, merely for the sacrosanctity
Hi Stefan,
when considering the prospective predicate equivalent to Id, I concluded
that the corresponding pred_set_conv rule should read:
lemma [pred_set_conv]:
HOL.eq = (\lambdax y. (x, y) \in Id)
by (auto simp add: Id_def fun_eq_iff)
However, for obvious reasons (LHS!), this should only
Hi Brian,
You had replaced Efficient_Nat.thy with a similar theory file named
Code_Numeral_Nat.thy. I chose to rename this back to Efficient_Nat
before doing the big merge, because it meant touching about a dozen
fewer files, and avoiding breaking lots of AFP entries. I also
reverted the
Hi Ondřej,
in
http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53
the name given to the derived theorem is unsatisfactory. Since it is
not a »code-only« theorem, it should not carry the »code« within. If it
would be a »code-only« theorem, the convention is to suffix with
I would strongly vote for qualified access:
Quotient.invariant
9 keys more to type, but very self-explanatory.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP
Hi Christian,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
there is a couple of issues you are hitting at here.
A. The (re-)introduction of the set type constructor
See
Hi all,
However, due to the deeper reason that the classical reasoner setup has
been changed so that the original proof failed, one might have to look
into this specific subgoal again (understanding how the classical
reasoner has been changed).
(I am guessing it is due to the
Hi *,
I am currently busy with stocktaking the results of my visit to TUM last
Wednesday, and I have updated the current state of two affairs in the wiki:
* The set story: https://isabelle.in.tum.de/community/Having_%27a_set_back
Not everything mentioned there is an ultimate need, but we should
Hi Lars,
I have now patches queued to enabled all of the commented out theorems
and pred_set_conv declarations, except for the generalited versions of
SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq
changes the theorems generated by inductive set in a negative way:
I have now patches queued to enabled all of the commented out theorems
and pred_set_conv declarations, except for the generalited versions of
SUP_UN_eq and INF_INT_eq. Using generalized versions of SUP_UN_eq
changes the theorems generated by inductive set in a negative way:
inductive_set
TFin
Hi Stefan,
I have fixed this bug now, see changeset b1d15637381a. Note that converting
the above theorem (and the other theorems in Relation.thy marked with FIXME)
to predicate notation requires the generalized versions of theorems
INF_INT_eq2 and SUP_UN_eq2, which should replace the more
Hi all,
recently I did some work to setup Stefan's ancient pred_set_conv utility
for relation predicates like sym(p) etc., see
http://isabelle.in.tum.de/reports/Isabelle/file/tip/src/HOL/Relation.thy
A few couple of things then came to surface:
* Naming: »inductive_set foo« yields »foop« as the
but I would
suggest waiting a week or two for the new import and trying to get
the maps correct there.
Ack.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital
4 months after Isabelle2011-1 we are roughly in the middle between two
official releases. This is a good point to recollect things for the
coming release, better than a few weeks before actual rollout (which
will the time for testing the integrated system, not adding new features).
In
With hg rev 07f9eda810b3: dependencies on ML files declared in theory
header are not resolved properly, e.g. try to edit
src/HOL/Import/HOL4Setup.thy
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Accidentally I have pushed something into the main repository which was
still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200
and continue with the other head.
Sorry for this,
Florian
--
PGP available:
Hi Lukas,
Am 24.02.2012 09:09, schrieb Lukas Bulwahn:
On 02/18/2012 10:18 AM, Florian Haftmann wrote:
How much relative time do the quickcheck examples in HOL-ex take?
According to my feeling time could be high to separate these into a
separate session, to facilitate maintenance.
I
Hi all,
It is also possible to have .hg/hgrc specific to individual repository
clones. So if testboard users are instructed to augment only that
hgrc with the evil option once and for all, the problem of getting
used to evil command lines in a different context is avoided.
This thread
Indeed. I would also prefer a server-side solution in the testboard
repositories (is there any way to permit a push generating new heads in
.hg/hgrc?)
A nice client-side solution is also:
[paths]
testboard = ssh://haftmann@macbroy//mnt/tmp/isatest/repositories/isabelle
[alias]
Hi all,
find attached some ideas for the future of quotient_type etc.
Time is too sparse to set everything out in detail here, but a few
corner stones:
* technical separation of lifting infrastructure (with a central role of
the »Quotient« predicate, theory Quotient_Lifting) with the
…an update with no sorry-proofs (I have been blinded by the obious…).
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
Quotient_Type_Definition.thy
Description: application/extension-thy
signature.asc
Hi all,
recently I stumbled again over our famour ancient README files, e.g.
http://isabelle.in.tum.de/dist/library/HOL/README.html.
Is there a vision what we should do with them in the long run?
Florian
--
PGP available:
Anyway, personally I have no strong opinion about this, so anybody who
wants to get hands on should feel invited to do so.
It would have been better to discuss such a change beforehand rather
than make it and then say that we are welcome to modify it.
Please recall:
The movement of the code
There were indeed some considerations before introducing List.fold into
Main HOL (being present in HOL-Library since around early summer 2010).
At some time I will set out them on the mailing list.
a) History: The fold in HOL-Library has been introduced by me at some
stage to accomplish
jEdit freezes after fast keystrokes in sequence in big theories: no
reaction on keyboard or mouse events, mouse pointer disappears; cpu load
of both poly and jvm processes is not conspicious.
Reproduction: Open List.thy with HOL-Plain as base image, edit something
in the middle of the
In plain old tty days one would get a traceback for exceptions atfer
ML {* Toplevel.debug := true *}
Is this trace somehow accessible by jEdit also?
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
instantiation list :: (order) order
begin
fun le_list :: ('a::order)list = 'a list = bool where
le_list [] [] = True |
le_list (x#xs) (y#ys) = (x = y xs = ys) |
le_list _ _ = False
*** exception Empty raised (line 331 of library.ML)
This seems to be a function-related issue, according
When having a look at
http://isabelle.in.tum.de/repos/isabelle/rev/39fe503602fb
it came to my mind that this might be implemented more generally, e.g.
the_aux :: 'a list = 'a
the_aux [x] = x
the :: 'a list = 'a
the xs = the_aux (remdups xs)
which would yield a Match exception without any
Hi all,
here my thoughts on the discussion:
a) release candidates – the announcements of release candidates indeed
could be a device for early feedback. The question is how to incite
users to take them more seriously.
b) development snapshots – I would prefer to get rid of them, providing
jEdit freezes after fast keystrokes in sequence in big theories: no
reaction on keyboard or mouse events, mouse pointer disappears; cpu load
of both poly and jvm processes is not conspicious.
Reproduction: Open List.thy with HOL-Plain as base image, edit something
in the middle of the theory;
The integration of the executable sets has lead me to the inclusion of
the canonical fold combinator on HOL lists (now List.fold :: ('a = 'b
= 'b) = 'a list = 'b = 'b) into the List theory corpus. In
connection with this I did a cleanup on the List.fold(l/r) material as
well. The idea is to
Next attempt on NEWS on sets committed.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
How much relative time do the quickcheck examples in HOL-ex take?
According to my feeling time could be high to separate these into a
separate session, to facilitate maintenance.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Jasmin,
Congratulations on your heroic effort for reintroducing set!
heroism and foolhardiness are close together…
I'm glad to report that Nitpick, Refute, Sledgehammer, and SMT_Example have
now been ported to handle set properly, and that the commented out examples
are live again.
Here is another change to be considered in the project of 'a set recovery:
changeset: 26814:b3e8d5ec721d
user:berghofe
date:Wed May 07 10:59:24 2008 +0200
files: src/HOL/Library/BigO.thy
src/HOL/Library/SetsAndFunctions.thy src/HOL/MetisExamples/BigO.thy
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent to prune any tinkering with
former theorems
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared.
Good news.
(https://isabelle.in.tum.de/isanotes/index.php/Having_'a_set_back%23Roaring_ahead).
Do not expect stability before this list has boilt down.
Not stability, but a working isatest
'set' is now a proper type constructor. Definitions mem_def and
Collect_def have disappeared. INCOMPATIBILITY, rephrase sets S used as
predicates by `%x. x : S` and predicates P used as sets by `{x. P x}`.
For typical proofs, it is often sufficent to prune any tinkering with
former theorems
Unfortunately, the find_theorems command is quite ignorant to any means
to hide facts:
Facts that have been hidden, can be found.
Note that with »hide« you do *not* hide the artefacts, but their name
access. The artefacts are still there. You can still argue that anyway
find_theorems etc.
Dear all,
since my post on quotient and partiality created some confusion, I want
to cast some light on it from a more direct perspective.
Concerning »typedef«, we currently have two conflicting issues:
a) From a foundational perspective, we want to leave »typedef« untouched
»as it is«
b)
Hi Christian,
with the below jedit_build component (is there a newer one?) and the
Isabelle repository version a61510361b89, after building jedit with
(isabelle jedit -f), The README under Prover Session is not shown and
more importantly also Output stays empty. Do others experience the
same
Hi all,
I'm asking myself the question how one would define rational numbers
using the quotient package. The key issue is that the equivalence
relation here is partial, ruling out denominators of value zero. In the
Isabelle reference manual I can find »partial:« in a syntax diagram but
not any
Hi Brian,
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].
I would welcome any
class neg_numeral = group_add + one
definition (in neg_numeral) neg_numeral :: bin = 'a where
neg_numeral k = - numeral k
Is there a conceptual point for neg_numeral, beyond concrete syntax issues?
One could just use regular uminus, but then there will be an accidental
change in
Hi Johannes,
two remarks:
* http://isabelle.in.tum.de/reports/Isabelle/rev/e828ccc5c110
With `notepad` you can prove everything without a trace in theory, which
eliminates the need for fiddling around with quick_and_dirty.
* http://isabelle.in.tum.de/reports/Isabelle/rev/34d07cf7d207
I would
@Florian: Is it imaginable to add such unsound setup
in a way that it does not infect the evaluation oracle by default?
Indeed. More on that another time (when I find some time).
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Christian,
please find attached the formalization of the merge-sort algorithm as
used in GHC's standard library. See also:
http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/Data-List.html#sort
interesting to read that comment. The exiting quicksort implementation
in
We are preparing for roaring ahead:
https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Dear all,
please keep in mind that we are on track to (re-)introduce a type
constructor for sets. I ask for solidarity: take this into account when
writing type annotations:
http://isabelle.in.tum.de/reports/Isabelle/file/2dd44cd8f963/src/HOL/Transitive_Closure.thy#l781
This should read:
Hi Lukas,
The issue can be observed at
http://isabelle.in.tum.de/reports/Isabelle/report/5497697969e943bda524c4b01be7d12e
Checking that the generated code in the Depth-First-Search AFP entry
actually compiles with ML is a minor point anyway, so I did not dig into
the details, but removed
Hi Lukas,
+text {* Definitions could be moved to Transitive_Closure if they are
of more general use. *}
is there any striking reason *not* to do so in the first place? At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.
In my opinion it is high time to
A further remark:
1.17 +definition ntrancl :: ('a * 'a = bool) = nat = ('a * 'a =
bool)
1.18 +where
1.19 + [code del]: ntrancl R n = (UN i : {i. 0 i i = (Suc n)}. R ^^
i)
Canonically and keeping in mind the upcoming 'a set, this would be
definition ntrancl :: nat = ('a *
Things like code generation might be of the form of associating document
content that is generated by functional evaluation over the semantics of
the formal source text. Think of it as part of browser_info, not the
src tree. Part of the question is who or what is the target of
generated
Hi again,
the current state of affairs concerning 'a set can be followed there:
https://isabelle.in.tum.de/isanotes/index.php/Having_%27a_set_back
Although I'd appreciate to see progress there, I do not ask to distract
any attention from tasks for the upcoming release.
Two remarks concerning
Hi Johannes,
I tried to reduce the runtime requirement of HOL-Probability by removing
some of the sublocale instantiations. As a lot of time is spend in
locale interpretation inside proofs.
Is the same interpretation repeated over and over? In that case the
corresponding proposition can be
Hi Brian,
After the release, I'll have to think about doing a complete overhaul
of all of the cancellation simprocs.
You are very welcome to do so. Before you start, call on me and I will
write down some ideas I had long ago (other may want to join, too).
Cheers,
Florian
--
Home:
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 instantiate foundational theorems of
locale with OF. Indeed, huge parts of
Hi Lukas,
the rename
AssocList ~ AList_Impl
should sound
AssocList ~ AList
Nota bene:
T.thy – theory as intended to be used by other theoreis
T_Impl.thy – implementation for abstract type
Since ALists are not abstract, there is no AList_Impl.thy, but cf.
RBT_Impl.thy.
The rename
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.
Thanks a lot, I have overlooked the other occurence.
I suggest to move the symbolic name identifier to code_target and
reference it uniformly from all ocurrences.
Florian
--
Home:
http://www.in.tum.de/~haftmann
Hi again,
thanks Alex for the summary.
So, it seems that we can conclude that instead of the nice unified
development that we hoped for in 2008, we got quite a bit of confusion
(points 1.1 and 1.2), in addition to the drawbacks that were already
known (1.3, 1.5-1.6). If we had to choose
Since August is the canonical time for vacation for many people it is
probably better to get into more concrete discussions in 3-4 weeks from
now, but people can already start thinking about their own areas of
responsibility concerning consolidation for the release.
I have two topics on the
When I've seen the complete_boolean_algebra incident on the other
thread my first impulse was to check how far the wiring of the class
package wrt. the Isabelle document markup was. In principle the prover
can provide useful clues in non-intrusive ways here, if done right.
E.g. in
(BTW, in
Scala ambiguity after additional imports is treated as an error, and
causes the conflicting name entries to be canceled out.)
I definitely like this!
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Should we ask a wider audience (isabelle-users) if anybody else has good
reasons against/for a change?
The thought deserves attention, but I think the discussion is too early
for that.
Indeed, this is where, as I deem, we current are:
* Some agreement that mixing sets and predicate syntax in
Hi all,
thanks to many efforts (thanks particularly to Alex, Brian, Cezary,
Larry) we already have gained some insights whether and how it would be
technically possible to introduce a set type constructor.
As I see the whole story, we have to think carefully how we would
proceed in order to
Hi Jasmin,
HOL-Metis_Examples FAILED
HOL-Nitpick_Examples FAILED
I can look into those things if and when it is decided to move to sets.
in case, thanks for the offer. Please ignore any further announcements
of these sessions in intermediate reports ;-).
Florian
--
Home:
Hi all,
I remember that once there was a discussion how AFP theories could be
referenced in theory headers using an environment variable AFP_THEORIES
or something similar.
Maybe the afp could be turned into an optional Isabelle component, e.g.
at ~~/contrib/afp. This would be have a couple of
maybe also declare them [no_atp], to avoid sledgehammer-generated proofs
that we know are going to break one release later...?
Maybe better now, as long as there are real sledgehammer-generated
proofs depending on it.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Larry,
And I'm finding it very difficult to work with two different versions of
Isabelle. I need to keep compiling one version or the other in order to
run tests. I know that we have ISABELLE_IDENTIFIER to eliminate that
problem, but it's empty in both versions.
I achieve this by having
I'm starting to have doubts about this entire procedure.
I thought the plan was to get these theories (particularly in the AFP) into a
state where they no longer dependent on confusing sets with predicates so
that they would work with either version of Isabelle. I'm not sure that's
A proof works only if I insert before it the following:
instance set :: (type) complete_boolean_algebra
proof
qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def Inf_bool_def
Sup_bool_def)
this is strange because this exact text already appears in the file
Complete_Lattice.thy
This suggestion looks promising. However, my impression is that
ISABELLE_OUTPUT specifies where images will be written to. Does it also
specify where images (unless a full path is specified) are read from? I often
seem to get the wrong image unless I rename them manually, which is obviously
Hi all,
Shouldn't one remove quite a bit of duplication first? The classes
distributive_complete_lattice and complete_boolean_algebra are now part
of HOL (the former as complete_distrib_lattice) (see the FIXME). The set
instances for those should be in/go into Florian's HOL repository as
Hi again,
Indeed, I think a general point can be made here, and not just about code
generation. In the last couple of years, we've run into situations in
Quickcheck, Nitpick, the code generator, and perhaps more, where we felt the
need for sets as different from functions. However, there
Hi again,
inquit Brian:
Overall, I must say that I am completely in favor of making set a
separate type again. But I also believe that the sets=predicates
experiment was not a waste of time, since it forced us to improve
Isabelle's infrastructure for defining and reasoning about predicates:
Hi again,
thanks to all contributors who already started to sort out some of the
set-pred mixture issues.
I have merged recent changes back into
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ -- this
is meant as a mere basis for figuring out problems experimentally, not
as a
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 pretty sure there are further ones either pro or contra,
for which
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
This is by no means meant as a thorough treatment of the whole
Dear all,
with Cezary's guidance, I set up mira configurations for building the
proofs bundle from the HOL Light repository and for running the
HOL-Generate-HOLLight with that bundle, cf.
http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3
for the first
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).
I think it might be useful to do to class number
what we did with class power a while back: Replace the overloaded
constant with a single, standard definition.
This would indeed be a valuable goal.
In any case, I think such a major change would require a bit of
planning, and probably won't
A more drastic solution would be to just get rid of the number class
altogether (its sole purpose seems to be so that you can have types
where numerals have a non-standard meaning) and have a single
definition of number_of that works uniformly for all types.
This would indeed be helpful, but
I want to add:
It is still used
(a) for didactical reasons, to teach primitive recursion over datatypes,
(a') to clearly indicate what the corresponding induction rule is.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Gerwin,
Is anyone prepared to leak Florian's new email address so I may haunt him?
I am prepared to be haunted ;-), I am still on the users and dev mailing
list and will follow them following the walrus strategy (only dive up
instantly if you think it is necessary).
First, a quick and dirty
By chance I discovered that the Isar Implementation Manual in the
release candidate is outdated and does not build from source.
My personal situation does not allow me to correct this personally, but
it should be easily accomplished.
All the best,
Florian
--
Home:
FYI.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
attachment: stat_cs.png
signature.asc
Description: OpenPGP digital signature
Hi all,
it seems indeed that JinjaThreads since recently runs out of memory even
on macbroy2 with parallelism, c.f. last afp isatest log:
Running HOL-Word-JinjaThreads ...
poly(19058,0xa00a0540) malloc: *** mmap(size=16777216) failed (error code=12)
*** error: can't allocate region
*** set a
501 - 600 of 672 matches
Mail list logo
