Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Bill Richter]

John, thanks for writing the code for me, but you only handled I think
my question about showing that the type of Tarski models is nonempty.
I should try to port your solution to Mizar.  Most of what else you
said was too advanced for me to respond to, but I'll work on it.

Makarius, I (following Freek) tend to think that Isabelle might be the
best language for high school teaching axiomatic proofs, but Isabelle
is intimidating, lots of programs to install & lots of dox.  If you
could start porting my Mizar code so I could see the pattern

I'm gratified folks want to read my paper where I fixed a longstanding
combinatorial error in homotopy theory.  It's on my web page
http://www.math.northwestern.edu/~richter/RichterPAMS-Lambda.pdf Maybe
I don't teach at NWU, but I did long ago, and they let me use the
computers so I can write such papers.  I called the error a `serious
pedagogical gap', as the results were proved in the literature, but
newcomers might easily leave the subject when told these results were
trivial (their teachers didn't know the combinatorial proofs).  There
are much more serious problems.  Recently lots of top conjectures
fell: Fermat's Last Theorem, the Poincare conjecture, Bieberbach's
conjecture, the Kervaire invariant conjecture (in my subject, homotopy
theory), and I don't have any confidence in these proofs.  Nobody in
my subject buys the proof of the Immersion conjecture
http://en.wikipedia.org/wiki/Whitney_immersion_theorem 
So I'm really impressed by Tom Hales for saying, ``I'll show I really
have a proof by using HOL, Coq, Isabelle etc for 20 man years''.

Cris, thanks for sending me the link of new_axiom, which I misread.  I
see now that reference.pdf clearly says that `new_axiom' should only
be used basically to add in new axioms to ZFC, such as large
cardinals.  But `new_definition' looks fine:

   Evaluating `new_definition' ‘c v_1 ... v_n = t‘ where c is a
   variable [...]  returns the theorem:
  |- !x_1 ... x_m. c v_1 ... v_n = t

That looks like an axiom to me.  My only problem is that I don't know
how to write declarative code in HOL.  As I posted, I can't get any any
of the mizar modes to work for me, including Freek's latest miz3.miz.
But I contend that mizar modes should not be needed.  The main thing I
like about Mizar is just that it's declarative and I can break proofs
up into cases and do proofs by contradiction.  We really don't want a
powerful theorem prover in high school geometry!  We want the kids to
have to write down most of the steps.  And unless I'm really
misunderstanding Mizar, Mizar would not be a good language for the
kids to program in.   Any Mizar experts who want to explain 
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
how I'm doing it all wrong, I'd be grateful.  

Roger, thanks for the code.  Hartshorne explains this

   I do not have the impression that Hilbert was thinking much of
   Euclid's elements 

I read much of Greenberg's book with no idea whatsoever why Hilbert
came up with his axioms, but after reading Hartshorne's book, the
light went on: Hilbert was fixing Euclid!  I think this is well-known.
Hilbert made a lot more sense after I realized that.  Hartshorne's
book is great anyway, and I fixed some proofs of his in my paper.
http://www.math.northwestern.edu/~richter/hilbert.pdf

   or had any particular interest in improving on its rigour.

I'm sure that's wrong, but this probably isn't the place to discuss
it.  Read Greenberg, who explain that Euclid's angle-addition errors
weren't found until they discovered non-Euclidean geometry.

   Indeed, from the point of view of rigour it takes some forward and
   some backward steps.

I don't know what you mean by backward steps.  Greenberg & Hartshorne
don't mention any.

-- 
Best,
Bill 

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL Constant Definition Done Right

[Rob Arthan]

On 25 Apr 2012, at 14:03, Ramana Kumar wrote:

> Looks like interesting conversations. Congratulations on doing such a great 
> job of writing them up! I would be more than happy to fix the relevant 
> OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light 
> adopt this proposal.
> 
> One small comment: in the description of the revised new_specification, there 
> is a capital "P" (below the words "the following axiom:") that should 
> probably be lowercase (or else I misunderstood something).
>
Thanks for the feedback - you are quite right, the "P" should be "p".

Regards,

Rob.
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[John Harrison]

Hi Bill,

| Thanks for the responses!  Can someone look at the code I posted
| http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar
| and tell me how to turn it into nice HOL code?  Or post a different
| axiom-proof example? There's no relevant example in the HOL dox.

There are two different issues, I suppose: first setting up the
axiomatic basis, and secondly actually doing the proofs. I'll comment
a bit more on setting up the axioms below. For the proofs, you already
have scripts in Mizar, and this style seems better suited to the
domain, so you may want to consider using one of the "Mizar Light"
like systems within HOL Light (see reply from Freek in the other
thread). There is already lots of interesting work going on in
Edinburgh on formalizing geometry using HOL Light, which indeed uses
Mizar Light. I'll leave those involved to tell you more details, but
you can find the following recent papers online by Phil Scott and
Jacques Fleuriot:

 "An Investigation of Hilbert's Implicit Reasoning Through
  Proof Discovery in Idle Time" (ADG 2010)

 "Composable Discovery Engines for Interactive Theorem Proving"
  (ITP 2011)

| Lorenzo, I'd be delighted to see your Tarski geometry code, but if you
| could explain how to do it on the group, that might be even better.

I didn't see this email, but it sounds interesting.

| Roger, if there's ``some cultural aversion to the use of axioms in the
| HOL community,'' then maybe HOL isn't the right proof-checker to use
| in high school geometry classes.  Does anyone think there is a better
| proof-checker?  My guess is that this is just an interface problem
| that HOL could easily solve, and I'm willing to work on it myself.

It's not so much that HOL prevents you from reasoning axiomatically if
you want to, merely that the "house style" is to build up everything
definitionally. In fact, this was one of the features that
distinguished HOL from its LCF-like predecessors.

As Makarius suggested, one approach is to make all your theorems
hypothetical with the "axioms" as the antecedent of an implication.
This could be done, but since HOL Light doesn't have any built-in
module or sectioning mechanism, you would need to set up a bit of
machinery yourself to avoid seeing these assumptions pop up in a few
places.

Another approach, which would work more smoothly in HOL Light at
least, is to set up a new type isomorphic to some specific model, but
then merely derive the axioms and thereafter reason from them alone,
never looking back at the respresentation. (Rather as one might
consider real numbers as being Dedekind cuts but then never look back
at the definitions once the complete ordered field axioms are
derived.) This is not unlike what you have done in Mizar already, as
noted in this comment:

  :: In Mizar it isn't possible to define such a type (or model) without
  :: proving that some model exist

It would be pretty easy to prove most of the axioms for real^2 based
on the theory already there in the "Multivariate/..." theories. Then
the process of setting up a new type corresponding to it is a little
bit technical but basically straightforward. For example, here is a
possible start:

  (* --- *)
  (* Define a new type "Plane" in bijection with real^2. *)
  (* --- *)

  needs "Multivariate/determinants.ml";;

  let Plane_TYBIJ =
let th = prove(`?x:real^2. T`,REWRITE_TAC[]) in
let def = new_type_definition "Plane" ("planify","coords") th in
REWRITE_RULE[] def;;

  (* --- *)
  (* Define notions of congruence and between-ness as Euclidean equivalents. *)
  (* --- *)

  parse_as_infix("===",(12, "right"));;

  let Congruent_DEF = new_definition
   `a,b === c,d <=> dist(coords a,coords b) = dist(coords c,coords d)`;;

  let Between_DEF = new_definition
   `Between (a,b,c) <=> between (coords b) (coords a,coords c)`;;

  (* --- *)
  (* Simple tactic to switch variables from "Plane" to "real^2". *)
  (* --- *)

  let PLANE_COORD_TAC =
let PLANE_QUANT_THM = MESON[Plane_TYBIJ]
  `((!x. P x) <=> (!x. P(planify x))) /\
   ((?x. P x) <=> (?x. P(planify x)))`
and PLANE_EQ_THM = MESON[Plane_TYBIJ] `planify x = planify y <=> x = y` in
REWRITE_TAC[PLANE_QUANT_THM; Congruent_DEF; Between_DEF; PLANE_EQ_THM;
Plane_TYBIJ];;

  (* --- *)
  (* Derivation of the axioms.   *)
  (* --- *)

  let AXIOM_1 = prove
   (`!a b. a,b =

Re: [Hol-info] newbie questions

[John Harrison]

Hi Felix,

Many of your questions have been well answered already by Petros and
Mark, but here are some comments on two items:

| 2) Where are definitions stored, anyway? There seems to be some global
| state involved. Is there a way to make definitions locally? Or to pass
| definitions around explicitly?

At the moment, the definitions are just stored in a mutable list, as you
say. The actual variable (see "the_definitions" in fusion.ml) is buried
in the logical kernel but you can inspect it by "definitions()", and of
course it gets extended when you make a definition.

In some ways it would be more elegant to remove such uses of mutable
state, which can probably be done without significantly compromising
simplicity or efficiency. See for example Freek Wiedijk's "Stateless HOL"
paper:

  http://arxiv.org/abs/1103.3322v1

| 3) HOL Light has large libraries for num, int and real. Are there also
| libraries for abstract groups, rings or fields?

Not in the standard distribution, anyway, though some people may well
have developed their own. Generally the mathematical theories included
in the core distribution are biased towards specific structures rather
than general axiomatic theories.

John.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] UITP'12: Final Call for Papers

[Cezary Kaliszyk]

[Apologies if you receive multiple copies]

*** Post-proceedings will appear in EPTCS ***



 --- Final Call for Papers ---

 10th International Workshop on
 User Interfaces for Theorem Provers (UITP 2012)
 11.07.2012, Bremen, Germany, Part of CICM 2012

   http://www.informatik.uni-bremen.de/uitp12/


While interactive theorem provers have found many new application
areas in the last years, the system interfaces have often not
enjoyed the same attention as the proof engines themselves. In
many cases, interfaces remain relatively basic and
under-designed. More and more, this is becoming an obstacle for
the wider adoption of theorem proving technologies outside the
academic community.

The User Interfaces for Theorem Provers workshop series provides
a forum for researchers interested in improving human interaction
with interactive proof systems, be it theorem provers, formal
method tools, and other tools manipulating and presenting
mathematical formulas.
For the forthcoming 10th UITP workshop, we invite contributions
from the theorem proving, formal methods and tools, and HCI
communities, both to report on experience with existing systems,
and to discuss new directions. Topics covered include, but are
not limited to:

 * Application-specific interaction mechanisms or designs for
   prover interfaces;
 * Experiments and evaluation of prover interfaces;
 * Languages and tools for authoring, exchanging and presenting
   proof;
 * Implementation techniques (e.g. web services, custom
   middleware, DSLs);
 * Integration of interfaces and tools to explore and construct
   proof;
 * Representation and manipulation of mathematical knowledge or
   objects;
 * Visualisation of mathematical objects and proof;
 * System descriptions.

Submitted papers should describe previously unpublished work
(completed or in progress), and not be longer than twelve
pages. We encourage concise but relevant papers. Submissions
should be in PDF format, and typeset with the EasyChair LaTeX
document class (which can be downloaded from www.easychair.org),
or in similar style.

Submission are via EasyChair. All papers will be peer reviewed by
members of the programme committee and selected by the organizers in
accordance with the referee reports.

Proceedings

Accepted papers will appear in the workshop proceedings, which will be
available in printed form at the workshop. After the workshop, revised
papers can be submitted to a postproceedings, which will appear in EPTCS.

Important Dates

 Submission deadline:  01.05.2012
 Acceptance notification:  01.06.2012
 Camera-ready copy:15.06.2012

Program Committee:

 David Aspinall, University of Edinburgh, UK
 Serge Autexier, DFKI, Germany
 Christoph Benzmueller, Articulate Software, USA
 Herman Geuvers, Radboud University Nijmegen, the Netherlands
 Cezary Kaliszyk, University of Innsbruck, Austria, (PC co-chair)
 Christoph Lüth, DFKI, Germany (PC co-chair)
 Adam Naumowicz, University of Białystok, Poland
 Claudio Sacerdoti Coen, University of Bologna, Italy
 Geoff Sutcliffe, University of Miami, United States
 Enrico Tassi, INRIA, France
 Josef Urban, Radboud University Nijmegen, the Netherlands
 Makarius Wenzel, Université Paris-Sud 11, France

-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL Constant Definition Done Right

[Ramana Kumar]

Looks like interesting conversations. Congratulations on doing such a great
job of writing them up! I would be more than happy to fix the relevant
OpenTheory importer/exporters if OpenTheory and/or HOL4 and/or HOL Light
adopt this proposal.

One small comment: in the description of the revised new_specification,
there is a capital "P" (below the words "the following axiom:") that should
probably be lowercase (or else I misunderstood something).

On Wed, Apr 25, 2012 at 12:42 PM, Rob Arthan  wrote:

> Conversations with Mark Adams and John Harrison at the Milner Symposium
> earlier last week inspired me to think through a new approach to defining
> constants in HOL. This generalises what was done in early versions of HOL
> Light. It constitutes an adjustment to new_specification that supersedes
> new_definition altogether and is less restrictive as regards the
> polymorphism of the defining axiom than the existing new_specification.
>
> I would welcome any comments anyone may have on this proposal, which can
> be found at http://www.lemma-one.com/papers/hcddr.pdf. Comments on the
> correctness or otherwise of any of the informal proofs in the proposal
> would be particularly welcome.
>
> Regards,
>
> Rob.
>
>
>
> --
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL Constant Definition Done Right

[Rob Arthan]

Conversations with Mark Adams and John Harrison at the Milner Symposium earlier 
last week inspired me to think through a new approach to defining constants in 
HOL. This generalises what was done in early versions of HOL Light. It 
constitutes an adjustment to new_specification that supersedes new_definition 
altogether and is less restrictive as regards the polymorphism of the defining 
axiom than the existing new_specification.

I would welcome any comments anyone may have on this proposal, which can be 
found at http://www.lemma-one.com/papers/hcddr.pdf. Comments on the correctness 
or otherwise of any of the informal proofs in the proposal would be 
particularly welcome.

Regards,

Rob.

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Makarius]

On Tue, 24 Apr 2012, Bill Richter wrote:

> Roger, if there's ``some cultural aversion to the use of axioms in the 
> HOL community,'' then maybe HOL isn't the right proof-checker to use in 
> high school geometry classes.  Does anyone think there is a better 
> proof-checker?  My guess is that this is just an interface problem that 
> HOL could easily solve, and I'm willing to work on it myself.

The strict definitional approach is mainly for foundational purposes, and 
for good reasons.  The HOL community usually quotes Bertrand Russel on 
that:

   The method of "postulating" what we want has many advantages; they are
   the same as the advantages of theft over honest toil.
   Introduction to Mathematical Philosophy, New York and London, 1919, p 71.

This means things like inductive definitions, datatypes, recursive 
functions are explicitly reduced to basic principles, not "axiomatized" by 
some magic ML code.  Moreover your own concepts should be defined 
properly, and results stated and proven explicitly.

Nonetheless, this does not prevent the user from working in a local 
context with parameters and assumptions in a quasi-axiomatic manner. 
Your results would then be releative to certain premises my_pred x y z ==> 
... in terms of the logical foundations.  By organizing such assumptions 
in a reasonable way, your application does not have to expose this to the 
end-user.

Don't ask me how to do that in HOL4, HOL-Light, ... though.  I am merely a 
guest on this mailing list.


Makarius

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light

[Bill Richter]

Thanks for the responses!  Can someone look at the code I posted
http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar 
and tell me how to turn it into nice HOL code?  Or post a different
axiom-proof example? There's no relevant example in the HOL dox.

Lorenzo, I'd be delighted to see your Tarski geometry code, but if you
could explain how to do it on the group, that might be even better.

Roger, if there's ``some cultural aversion to the use of axioms in the
HOL community,'' then maybe HOL isn't the right proof-checker to use
in high school geometry classes.  Does anyone think there is a better
proof-checker?  My guess is that this is just an interface problem
that HOL could easily solve, and I'm willing to work on it myself.

Most of what I know about HOL is that Tom Hales really fired me about
in his Notices article.  Have you read Tom's article 
www.math.pitt.edu/~thales/papers/turing.pdf
His focus seems quite different from mine.  I'd like to use
proof-checkers to rigorize human proofs, starting with high school
geometry. I've been appalled for some time at the lack of rigor in my
subject, homotopy theory, and even got a paper published 
http://www.ams.org/journals/proc/2009-137-07/S0002-9939-09-09763-9/S0002-9939-09-09763-9.pdf
fixing a longstanding error, and my first paragraph reads

   We find this to be a serious pedagogical gap and give combinatorial
   proofs here.

I'd like proof-checkers like HOL to improve the rigor level of
theorems that are much simpler that Tom's Kepler conjecture proof.
Tom's focus instead seems to be realizing Turing's AI dreams, and he
looks forward to the days of million page proofs churned out by the
computer, about which we can only understand `fables' which maybe are
churned out by the computer as well.  Then he laments that cosmic rays
may doom the enterprise.  It's an awe inspiring vision, and he has
lots of interesting example.  Perhaps it doesn't jibe with my focus.
Although using proof-checkers to debug software is a great idea.

John Harrison says that one route for debugging software is through
Denotational Semantics, which I know something about.  I failed on
comp.lang.scheme to explain to that there's a compositional semantic
function for Scheme that only uses only induction, and not Scott
models of the lambda calculus (basically non-Hausdorff Cantor sets).
Scott models are really cool, and give a new version of Church's
thesis: computable = continuous!  But you don't need Scott models for
a DS for Scheme.  It's almost obvious.  The standard reduction
function for the lambda calculus is perfectly well-defined (reduce the
leftmost lambda), and it only requires induction.  Keep performing
reduction steps until you're done, and if you're never done, send it
to bottom.  You can't write a program that will do that (by Turing's
solution to the Halting problem), but you can define this function
mathematically using only induction.  I even wrote a paper giving a
shorter proof that Barendregt's Normalization Theorem.
http://www.math.northwestern.edu/~richter/lambda-calc.pdf 
For Scheme we should use instead Felleisen's lambda value calculus,
where similar remarks apply.  We don't get a compositional semantic
function this way, of course, but that's easy to fix, using the usual
environment (& store if there's mutation), because Scheme is
compositional: you evaluate (x y) by first evaluating x to a function,
then evaluating y, and sending this value to the function.

-- 
Best,
Bill 

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Mizar Light and miz3

[Freek Wiedijk]

Dear everyone,

John Harrison pointed out to me that the following query was
posted on the hol-info mailing list (I'm subscribed to that
list but often just delete the messages without looking,
sorry about that.  So I missed this):

>6) I am very curious about Mizar Light and would like to convert
>my exercise to Mizar Light. I found the Mizar Light sources as
>well Freek's paper on Mizar Light. However, at first glance it
>seemed as if the syntax for Mizar Light given in the paper is
>quite different from what I saw in the source. So... what is the
>current status of the project?

There have been three experiments that I called "Mizar
Light".  However, after some soal searching I decided to
rename the third thing from "Mizar Light III" to "miz3",
so please don't call this third version Mizar Light
anymore... :-)

1. The first thing is described in a TPHOLs paper from
   2001, .
   _Conceptually,_ I still _really_ like this, but
   ergonomically it's completely unusable, because of all
   the quotes and brackets, and because it's really hard
   to debug proofs.  The Mizar proof

 Lm1: P implies P
 proof
   assume P;
   hence P;
 end;

   becomes in this framework:

 let lm1 = prove
  (`P ==> P`,
   ASSUME_A(0,`P:bool`) THEN
   THUS(`P:bool`) (BY [0][]));;

2. The second version never has been published about, but
   is part of the HOL Light distribution, it is in the
   sub-directory "Mizarlight".  It is an attempt to make
   the first version more ergonomic, while still keeping
   the property that a proof is just ocaml code, so without
   having a separate "Mizar parser".  In this system the
   above proof becomes:

 let lm1 = theorem
  "P ==> P"
  [assume "P";
   hence "P"];;

3. And then there's my recent "miz3" system, which
   is my current best effort, and which (very similar to
   John Harrison's "Mizar mode") _does_ have a separate
   parser that allows one to get really close to
   Mizar syntax.  It's described in the recent paper
   ,
   and the system can be downloaded as
   .  In this
   system the example is:

 let lm1 = thm `;
  let P be bool;
  thus P ==> P
  proof
   assume P;
   thus P;
  end`;;

   (In miz3 all variables have to be bound, either in the
   formula or in the context, hence the "let" at the start.
   Also in miz3 "then" is implicit, hence the "thus"
   instead of the "hence".)

I hope this clears things up.  I guess the poster might
have been confused between the first and second, or second
and third version of the thing?

Ah yes, and if someone would like help with using miz3,
just mail me!

Freek

--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and 
threat landscape has changed and how IT managers can respond. Discussions 
will include endpoint security, mobile security and the latest in malware 
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info