How about providing a parse function time_of_string which turns
strings like 30s or 15ms into proper times, and possibly adding a
configuration option scheme for times (besides the existing bool, int
and string schemes)? It seems that this could and should be provided
be provided by the system to
Or timeout is universally in seconds, as an integer w/o unit.
Simpler or more flexible. I have no strong view.
Tobias
Sascha Boehme schrieb:
How about providing a parse function time_of_string which turns
strings like 30s or 15ms into proper times, and possibly adding a
configuration option
On Fri, 29 Oct 2010, Sascha Boehme wrote:
How about providing a parse function time_of_string which turns
strings like 30s or 15ms into proper times, and possibly adding a
configuration option scheme for times (besides the existing bool, int
and string schemes)? It seems that this could and
* New command 'partial_function' provides basic support for recursive
function definitons over complete partial orders. Concrete instances
are provided for i) the option type, ii) tail recursion on arbitrary
types, and iii) the heap monad of Imperative_HOL. See
HOL/ex/Fundefs.thy and
* Significantly improved Isabelle/Isar implementation manual.
Or this is how I've spent 3 very nice weeks in the south of Portugal.
See Isabelle/e4f1275820b2.
Makarius
___
Isabelle-dev mailing list
* Parallel and asynchronous execution requires special care concerning
interrupts. Structure Exn provides some convenience functions that
avoid working directly with raw Interrupt. User code must not absorb
interrupts -- intermediate handling (for cleanup etc.) needs to be
followed by
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
The log message, Naming in line now with multisets seems to suggest
that consistency was the main motivation for this change. However, the
change had rather the opposite effect, since the expand_*_eq pattern
is much more common in the libraries. (Full disclosure: some, but not
all, of these lemmas
I wanted to emphasize the mathematical concept, not the operational
view. And indeed, it is shorter. For functional objects the ext_iff
convention fits perfectly. For example, for polynomials we already have
poly_ext in one direction. I have to admit, though, that for pairs it
would be a bit
OK, this makes sense. It is nice to have the pair of lemmas foo_ext
and foo_ext_iff for each function-like type foo.
So do you propose that we rename all of the expand_*_eq lemmas that I
listed before? (It would also be good to make sure there is a
properly-named *_ext lemma corresponding to each
HOL: Scala (2.8 or higher) has been added to the target languages of
the code generator.
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:
Abolished symbol type names: prod and sum replace * and +
respectively. INCOMPATIBILITY.
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:
'code_reflect' allows to incorporate generated ML code into
runtime environment; replaces immature code_datatype antiquotation.
INCOMPATIBILITY.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
* Pure: local theory specifications may depend on extra type variables
that are not present in the result type -- arguments TYPE('a) :: 'a itself
are added internally. For example:
definition unitary :: bool where unitary = (ALL (x::'a) y. x = y)
* Thoroughly revised locales tutorial. New section on conditional
interpretation.
Changes culminated over the last 12 months:
Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with
le_inf_iff
- dropped
New proof method smt for a combination of first-order logic
with equality, linear and nonlinear (natural/integer/real)
arithmetic, and fixed-size bitvectors; there is also basic
support for higher-order features (esp. lambda abstractions).
It is an incomplete decision procedure based on external
* New testing tool Mirabelle for automated (proof) tools. Applies several
tools and tactics like sledgehammer, metis, or quickcheck, to every proof step
in a theory. To be used in batch mode via isabelle mirabelle.
* GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm of
finite and
infinite sets. It is shown that they form a complete lattice.
* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in
DERIV_intros
assumes composition with an additional function and matches a variable
to the
derivative, which has to be solved by the simplifier. Hence
(auto intro!: DERIV_intros) computes the derivative of most elementary
terms.
*
*** ML ***
* More systematic treatment of long names, abstract name bindings, and
name space operations. Basic operations on qualified names have been
move from structure NameSpace to Long_Name, e.g. Long_Name.base_name,
Long_Name.append. Old type bstring has been mostly replaced by
Dear Isabelle developers,
we are now heading towards the next Isabelle release.
Since Isabelle 2008 a lot of changes and improvements have found their
way into the sources. For this reason I would kindly invite you all to
update the NEWS and CONTRIBUTORS in the root of the repository to
* HOL/Ring_and_Field and HOL/OrderedGroup: The lemmas group_simps and
ring_simps have been replaced by algebra_simps (which can be
extended with
further lemmas!). At the moment both still exist but the former will
disappear
at some point.
* Proofs of fully specified statements are run in parallel on multi-core
systems. A speedup factor of 2-3 can be expected on a regular 4-core
machine, if the initial heap space is made reasonably large (cf. Poly/ML
option -H). [Poly/ML 5.2.1 or later]
* High-level support for
On Tue, 23 Dec 2008, Makarius wrote:
* Proofs of fully specified statements are run in parallel on multi-core
systems. A speedup factor of 2-3 can be expected on a regular 4-core
machine, if the initial heap space is made reasonably large (cf. Poly/ML
option -H). [Poly/ML 5.2.1 or
* HOL: command 'atp_messages' displays recent messages issued by automated
theorem provers. This allows to examine results that might have got
lost due to the asynchronous nature of default 'sledgehammer' output.
(This acknowledges the fact that sledghammer occasionally breaks the
Makarius wrote:
Of course, heaps produced inside the repository file space like that must
not be committed.
We might want to add an .hgignore file and put ^heaps/ in it. This should at
least make accidental commits less likely.
Gerwin
Makarius wrote:
It is already there, together with some other things that people tend to
commit by accident:
Too fast for me ;-)
Gerwin
On Tue, 2 Dec 2008, Tjark Weber wrote:
On Sun, 2008-11-30 at 14:08 +0100, Makarius wrote:
The old isabelle-interface wrapper could react in confusing ways if
the interface was uninstalled or changed otherwise. Individual
interface tool configuration is now more explicit, see also the
On Tue, 2 Dec 2008, Tjark Weber wrote:
On Sun, 2008-11-30 at 13:03 +0100, Makarius wrote:
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
old ~/isabelle, which was slightly non-standard and apt cause
surprises on case-insensitive file-systems, or when working with
On Wed, 3 Dec 2008, Gerwin Klein wrote:
Makarius wrote:
Of course, heaps produced inside the repository file space like that must
not be committed.
We might want to add an .hgignore file and put ^heaps/ in it. This should at
least make accidental commits less likely.
It is already
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the
old ~/isabelle, which was slightly non-standard and apt cause
surprises on case-insensitive file-systems, or when working with local
copies of the Isabelle repository.
INCOMPATIBILITY, need to move existing ~/isabelle/etc,
* HOL/Finite_Set: added a new fold combinator of type
('a = 'b = 'b) = 'b = 'a set = 'b
Occasionally this is more convenient than the old fold combinator which is
now defined in terms of the new one and renamed to fold_image.
Tobias
* Dropped locale element includes. This is a major INCOMPATIBILITY.
In existing theorem specifications replace the includes element by the
respective context elements of the included locale, omitting those that
are already present in the theorem specification. Multiple assume
elements of a
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for
Poly/ML 5.2.1 or later.
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
hypotheses. Sorts required in the course of reasoning need to be
covered by the constraints in the initial statement, completed by the
type instance information of the background theory. Non-trivial sort
hypotheses, which
* Generic ATP manager for Sledgehammer, based on ML threads instead of
Posix processes. Avoids potentially expensive forking of the ML process.
New thread-based implementation also works on non-Unix platforms
(Cygwin). Provers are no longer hardwired, but defined within the theory
via plain ML
* Unified theorem tables for both code code generators. Thus [code
func] has disappeared and only [code] remains. INCOMPATIBILITY.
--=20
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_in=
formatik_tu_muenchen_de
-- next part --
A
* Simplified main Isabelle executables, with less surprises on
case-insensitive file-systems (such as Mac OS).
- The main Isabelle tool wrapper is now called isabelle instead of
isatool.
- The former isabelle alias for isabelle-process has been
removed (should rarely occur to regular
* Wrapper script for remote SystemOnTPTP service allows to use
sledgehammer without local ATP installation (Vampire etc.). See also
ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
variable. (By Fabian Immler, TUM)
(CVS note: need to move Distribution/contrib/ out of the way, if
Normalization by evaluation now allows non-leftlinear equations.
Declare with attribute [code nbe].
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-- next part --
A non-text attachment
* The Isabelle emacs tool provides a specific interface to invoke
Proof General / Emacs, with more explicit failure if that is not
installed (the old isabelle-interface script silently falls back on
isabelle-process). The PROOFGENERAL_HOME setting determines the
installation location of the Proof
* Name bindings in higher specification mechanisms (notably
LocalTheory.define, LocalTheory.note, and derived packages) are now
formalized as type Name.binding, replacing old bstring.
INCOMPATIBILITY, need to wrap strings via Name.binding function, see
also Name.name_of. Packages should pass name
I think for cvs version this is Isabelle/Distribution/lib
subsdirectory.
Michael Nedzelsky
I don't have a lib subdirectory and cvs does not know about one.
Tobias
Makarius schrieb:
*** System ***
* Isabelle/lib/classes/Pure.jar provides basic support to integrate
the Isabelle process
On Sun, 24 Aug 2008, Tobias Nipkow wrote:
I don't have a lib subdirectory and cvs does not know about one.
The NEWS are always in terms of a proper distributions, for users out
there. The CVS layout is a bit mangled, and lib is in Distribution/lib.
Makarius
* @{lemma} in latex and ML: allow initial and terminal method expressions,
as in the Isar command 'by'.
* @{lemma} in ML now closes the derivation, unless @{lemma (open) ...} is
specified.
*** HOL-NSA ***
* Created new image HOL-NSA, containing theories of nonstandard
analysis which were previously part of HOL-Complex. Entry point
Hyperreal.thy remains valid, but theories formerly using
Complex_Main.thy should now use new entry point Hypercomplex.thy.
My $0,02: I was wondering about the merge as well. For my taste, there is
almost too much in HOL already as it is.
It's not such a big problem, though. You can always build your own custom
images with exactly the part you need (not that it's a nice user-interface
paradigm, and you need to
Very nice job!
Amine.
PS: In Reflected Ferrack you start combutation with True, i.e. @{code
T}, if the input is @{term False}. Fortunately this does not happen
often Even with @{code} we still need to be careful...
Florian Haftmann wrote:
New ML antiquotation 'code': takes constant as
* Integrated image HOL-Complex with HOL. Entry points Main.thy and
Complex_Main.thy remain as they are.
* New image HOL-Plain provides a minimal HOL with the most important
tools available (inductive, datatype, primrec, ...). By convention the
corresponding theory Plain should be ancestor of
* ML: Disposed old term read functions (Sign.read_def_terms,
Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.).
INCOMPATIBILITY, should use regular Syntax.read_term,
Syntax.read_term_global etc.; see also OldGoals.read_term as last
resort for legacy applications.
* ML: rules and tactics that read instantiations (read_instantiate,
res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof
context, which is required for parsing and type-checking. Moreover,
the variables are specified as plain indexnames, not string encodings
thereof.
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
INCOMPATIBILITY, object-logics depending on former Pure require
additional setup PureThy.old_appl_syntax_setup; object-logics
depending on former CPure need to refer to Pure.
* More flexible generation of measure functions for termination proofs:
Measure functions can be declared by proving a rule of the form
is_measure f and giving it the [measure_function] attribute. The
is_measure predicate is logically meaningless (always true), and
just guides the heuristic. To
* Theory Int: The representation of numerals has changed. The infix operator
BIT and the bit datatype with constructors B0 and B1 have disappeared.
INCOMPATIBILITY, use Int.Bit0 x and Int.Bit1 y in place of x BIT bit.B0
and y BIT bit.B1, respectively. Theorems involving BIT, B0, or B1 have been
* Theory loader: use_thy (and similar operations) no longer set the
implicit ML context, which was occasionally hard to predict and in
conflict with concurrency. INCOMPATIBILITY, use ML within Isar which
provides a proper context already.
Dear all,
quickcheck can now also display counterexamples involving functions (using
notation for function updates). For example,
consts app: ('a = 'a) list = 'a = 'a
primrec
app [] x = x
app (f # fs) x = app fs (f x)
lemma app (fs @ gs) x = app fs (app gs x)
quickcheck
On Sun, 6 Jan 2008, Makarius wrote:
* Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), based on
Isabelle/JVM process wrapper (see Isabelle/lib/classes). Note that the
precompiled jars are only available in a proper distribution, but not in
the internal CVS (cf.
Instantiation target allows for simultaneous specification of class
instance operations together with an instantiation proof. Type check
phase allows to refer to class operations uniformly. See
HOL/Complex/Complex.thy for an Isar example and HOL/Library/Eval.thy for
an ML interface example.
* System: polyml-platform script now identifies x86_64-linux with
x86-linux, which is usually more efficient. INCOMPATIBILITY, requires
manual settings if x86_64-linux is really intended (e.g. for 2GB heap
or 64MB stack).
* ML/Isar: simplified interfaces for outer syntax. Renamed
OuterSyntax.add_keywords to OuterSyntax.keywords. Removed
OuterSyntax.add_parsers -- this functionality is now included in
OuterSyntax.command etc. INCOMPATIBILITY.
* Pure/Isar: unified syntax for new-style specification mechanisms (e.g.
'definition', 'abbreviation', or 'inductive' in HOL) admits full type
inference and dummy patterns (_). For example:
definition K x _ = x
* The transitivity reasoner for partial and linear orders is set up for
locales `order' and `linorder' generated by the new class package.
Previously
the reasoner was only set up for axiomatic type classes. Instances
of the
reasoner are available in all contexts importing or interpreting
* ML basics: just one true type int, which coincides with IntInf.int
(even on SML/NJ).
* HOL finally supports full list comprehensions as in Haskell, except
that . is used instead of |. As a by-product, pattern-matching
abstractions % pat1 = e1 | ... are supported as well.
I assume, `% pat1 = e1 | pat2 = e2' is equivalent to
% a0 . case a0 of pat1 = e1 | pat2 = e2
with `a0' being a fresh identifier.
Yes.
How does a multiple-arguments (automatically curried) lambda look like?
It doesn't exist. At least not in Isabelle.
BTW, list comprehension is
701 - 766 of 766 matches
Mail list logo
