[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy

2007-09-14 Thread Makarius
, a theory that does not depend on any unnecessarily strong axioms also seems to be more appealing from a foundational point of view. I agree with this. Makarius

[isabelle-dev] NEWS

2007-09-19 Thread Makarius
* ML basics: just one true type int, which coincides with IntInf.int (even on SML/NJ).

[isabelle-dev] NEWS

2007-09-26 Thread Makarius
* 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

[isabelle-dev] NEWS

2007-10-06 Thread Makarius
* 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.

[isabelle-dev] NEWS

2007-11-08 Thread Makarius
* 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).

[isabelle-dev] Isabelle sources at 0 Kelvin

2007-11-13 Thread Makarius
installation (homegrown Linux kernel, exotic Emacs version etc.), using the official binaries provided from the website. Makarius

[isabelle-dev] prems

2007-11-22 Thread Makarius
are marked up uniformly using font-lock-reference-face, which happens to default to red in XEmacs, but something else in GNU Emacs. In any case, you are free to redefine the face in any way you like, e.g. using the Edit Faces menu. Makarius

[isabelle-dev] NEWS

2008-01-07 Thread Makarius
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. Admin

[isabelle-dev] NEWS

2008-01-27 Thread Makarius
* 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.

[isabelle-dev] record pretty printing

2008-02-13 Thread Makarius
. Makarius

[isabelle-dev] NEWS (update)

2008-05-18 Thread Makarius
* 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.

[isabelle-dev] NEWS

2008-06-16 Thread Makarius
* 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.

[isabelle-dev] NEWS

2008-06-19 Thread Makarius
* 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.

[isabelle-dev] HOL vs. HOL-Complex

2008-07-02 Thread Makarius
that there is no particular advantage in the NSA part anymore, unless you are specifically interested in the non-standard thing? Makarius

[isabelle-dev] NEWS (update)

2008-07-10 Thread 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.

[isabelle-dev] ProofGeneral history via Mercurial

2008-07-11 Thread Makarius
the parent directory of that URL. Note that this is a readonly copy of the official ProofGeneral CVS from Edinburgh. As usual, early adopters of PG pre-3.7.1 should post problem reports to http://proofgeneral.inf.ed.ac.uk/trac/ (you can just create your own account). Makarius

[isabelle-dev] NEWS

2008-08-24 Thread Makarius
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

[isabelle-dev] Fwd: Re: new isabelle interface

2008-08-25 Thread Makarius
to be on the right track already: keep with the separate process model. Apart from stability it also allows to run the prover and GUI an separate machines. (``Modern'' GUIs do need 1 or 2 cores for themselves, just to display things to the user.) Makarius

[isabelle-dev] new isabelle interface

2008-08-25 Thread Makarius
emerging) server infrastructure, I would be happy to assist them. Makarius

[isabelle-dev] new isabelle interface

2008-08-26 Thread Makarius
to put them back into the CVS. We are still working on getting more Isabelle people aquainted with Mercurial, so that we can get rid of CVS eventually. Makarius

[isabelle-dev] isabelle/repos

2008-08-02 Thread Makarius
to be de-centralized.) Makarius

[isabelle-dev] Relation_Power.thy

2008-09-02 Thread Makarius
input methods and proper display (without the flashing of x-symbol for \^sub for example). Makarius

[isabelle-dev] NEWS

2008-09-02 Thread Makarius
* 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

[isabelle-dev] Mercurial conversion relaunch

2008-09-03 Thread Makarius
On Wed, 3 Sep 2008, Makarius wrote: Within the next few hours http://isabelle.in.tum.de/repos/isabelle will recover to the present state of the CVS. Since this is a fresh Mercurial repository, local clones probably need to be recreated from scratch. In the mean tome it might be helpful

[isabelle-dev] [Fwd: Re: Find]

2008-09-12 Thread Makarius
. Makarius

[isabelle-dev] NEWS

2008-09-16 Thread Makarius
* 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

[isabelle-dev] [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)

2008-09-27 Thread Makarius
the magicians ;-) And the wizards ... Makarius

[isabelle-dev] Fwd: Broken link

2008-10-01 Thread Makarius
On Wed, 1 Oct 2008, Lawrence Paulson wrote: In fact, all the links to logics in the theory library section are broken. I have fixed this problem of Isabelle2008 already, and said so recently in an answer to somebody on isabelle-users. Makarius

[isabelle-dev] NEWS

2008-10-03 Thread Makarius
* 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

[isabelle-dev] NEWS

2008-10-04 Thread Makarius
* 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

[isabelle-dev] NEWS

2008-10-17 Thread Makarius
* 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

[isabelle-dev] Multicore performance preview

2008-10-21 Thread Makarius
On Tue, 21 Oct 2008, Stefan Berghofer wrote: Makarius wrote: You will need the latest Poly/ML 5.2.1 version to prevent a strange GC deadlock problem in 5.1/5.2. Where can I get the latest version? The latest version offered for download on the Sourceforge page http

[isabelle-dev] [polyml] Release 5.2.1 (fwd)

2008-10-22 Thread Makarius
Our usual packages for use with Isabelle are available here: http://isabelle.in.tum.de/polyml-5.2.1/ For any serious use of multithreading in recent development snapshots Poly/ML 5.2.1 is really required, but there is no immediate need to recompile the official Isabelle2008. Makarius

[isabelle-dev] NEWS (update)

2008-10-23 Thread Makarius
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for Poly/ML 5.2.1 or later.

[isabelle-dev] NEWS

2008-11-30 Thread Makarius
* 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,

[isabelle-dev] Isabelle on Mercurial

2008-11-30 Thread Makarius
, one could have both repositories active for a few days, and merge later using means of Mercurial, but things should be kept as simple as possible. Makarius

[isabelle-dev] Netbeans 6.5 and Scala

2008-11-19 Thread Makarius
of the official Netbeans repository yet, but see here http://blogtrader.net/page/dcaoyuan/entry/new_scala_plugin_for_netbeans This description is for 6.5 RC2 and works for 6.5 final unchanged. The plugin uses the current Scala 2.7.2.final. Makarius

[isabelle-dev] Directory layout

2008-12-01 Thread Makarius
, implementation) I have already used the @{file} document antiquotation to get a statically checked references to the Isabelle file space. Makarius

[isabelle-dev] Isabelle on Mercurial

2008-12-01 Thread Makarius
is installed in /home/isabelle-repository/repos/.hg/hgrc already, but the Mercurial security model prevents its execution if you are not wenzelm. This is what the warning Not trusting file ... refers to. Makarius

[isabelle-dev] NEWS (update)

2008-12-02 Thread Makarius
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

[isabelle-dev] NEWS

2008-12-02 Thread Makarius
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

[isabelle-dev] NEWS

2008-12-02 Thread Makarius
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

[isabelle-dev] Isabelle on Mercurial

2008-12-02 Thread Makarius
is to remove them gradually, or just ignore them for now. Makarius

[isabelle-dev] Isabelle on Mercurial

2008-12-02 Thread Makarius
should be done with great care. Makarius

[isabelle-dev] Isabelle on Mercurial

2008-12-02 Thread Makarius
On Tue, 2 Dec 2008, Tjark Weber wrote: On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote: With Mercurial you have the whole history always around, and there is no need to encode (tiny) parts of it in the file. Certainly $Id$ keys are rather useless as long as the file is part

[isabelle-dev] Isabelle on Mercurial

2008-12-02 Thread Makarius
. For the development snapshot the release name is the id of the changeset that makedist encountered as tip. If anybody uses the repository directly, not a release, then hg tip will provide that information. Makarius

[isabelle-dev] Usage Isabelle2007

2008-12-05 Thread Makarius
ProofGeneral-3.7.1 Normally there is no need to use the 64 bit version, unless you have something like 8 GB of real memory. The 32 bit version is a bit faster. Makarius

[isabelle-dev] ISABELLE_HOME/contrib vs. ISABELLE_HOME/..

2008-12-05 Thread Makarius
~/isabelle/ProofGeneral ~/isabelle/E ... With this layout there is no need to edit ~/.isabelle/etc/settings or create symlink etc. Makarius

[isabelle-dev] TortoiseHg: GUI for Mercurial

2008-12-11 Thread Makarius
://tortoisehg.wiki.sourceforge.net/hgtk For example, the hgtk log tool is similar to the old hg view (which was a bit ugly due to Tcl/Tk). Makarius

[isabelle-dev] NEWS

2008-12-15 Thread Makarius
* 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

[isabelle-dev] Mac OS Isabelle.app bundle

2008-12-22 Thread Makarius
or in Isabelle.app/../Isabelle Likewise for Emacs, but it is also found in /Applications/Emacs.app/Contents/MacOS/Emacs if available. The Mac OS application bundle is meant to become part of the next official Isabelle release, which is due within the next 2 months or so. Makarius

[isabelle-dev] NEWS

2008-12-23 Thread Makarius
* 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

[isabelle-dev] NEWS

2008-12-23 Thread Makarius
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

[isabelle-dev] More Mercurial hints

2009-02-02 Thread Makarius
not trusting the default hgrc of the central pull/push area can be disabled like this: [trusted] users = wenzelm This needs to be added to ~/.hgrc on the server side within the broy network at TUM. Makarius

[isabelle-dev] A better policy for the typerep class

2009-02-28 Thread Makarius
On Sat, 28 Feb 2009, Brian Huffman wrote: Quoting Makarius makarius at sketis.net: In particular, merging ATP_Linkup is a bit critical: if it is done via several unrelated paths, then some internal derivations are duplicated unnecessarily. (In fact, it used to crash here in the past, now

[isabelle-dev] More Mercurial hints

2009-03-04 Thread Makarius
On Mon, 2 Feb 2009, Makarius wrote: * Merges can be simplified by doing hg fetch frequently, especially just before starting to perform local edits. Also do not forget to push eventually, to give others a chance to pick up the changes. Note that excessively long merge edges

[isabelle-dev] More Mercurial hints

2009-03-04 Thread Makarius
I've found some nice illustrations on the web ... Mercurial: http://tinyurl.com/cxrbjt CVS:http://tinyurl.com/dk3gsz Makarius

[isabelle-dev] More Mercurial hints

2009-03-04 Thread Makarius
On Wed, 4 Mar 2009, Brian Huffman wrote: Quoting Makarius makarius at sketis.net: I've found some nice illustrations on the web ... Mercurial: http://tinyurl.com/cxrbjt CVS:http://tinyurl.com/dk3gsz So, you're saying that with Mercurial, you can do a lot more damage? Yes

[isabelle-dev] NEWS

2009-03-09 Thread Makarius
*** 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

[isabelle-dev] Forgotten feature of the datatype package

2009-05-28 Thread Makarius
old-style type names such as * which will still be with us for some time. In newer developments, those that are less than 10 years old, plain identifiers are used uniformly of course. Makarius

[isabelle-dev] Type error in metis call with Toplevel.debug

2009-06-15 Thread Makarius
General.) Makarius

[isabelle-dev] repos integrity

2009-06-18 Thread Makarius
AFP tests can come a bit later (hours or days, but not weeks). * Any user-relevant changes should be documented in NEWS (say within 1-2 weeks after a push, afterwards it is usually forgotton). * Any relevant contribution should get an entry in CONTRIBUTORS. Makarius

[isabelle-dev] Pending sort hypotheses

2009-07-02 Thread Makarius
? Makarius

[isabelle-dev] Clash of specifications

2009-07-03 Thread Makarius
with Plain. Makarius

[isabelle-dev] Bug Tracking

2009-07-09 Thread Makarius
of the component in question (usually the original author or main maintainer), it is usually introducing more problems than are resolved. Makarius

[isabelle-dev] Bug Tracking

2009-07-10 Thread Makarius
. If this is a plea for more maintainable code, one can hardly disagree. Documentation might help, as might unit tests. No, this refers to deep understanding what is really going on, not any superficial poking around with modern things that come and go every few years. Makarius

[isabelle-dev] Isabelle NEWS as a blog ?

2009-07-14 Thread Makarius
changes semantically to enable understanding of the history of sources many months or years later. Log entries of the form now we have finished this or now we have fixed that would be usually wrong anyway. Makarius

[isabelle-dev] Isabelle/HOL --- the missing history

2009-07-23 Thread Makarius
quite bulky and taking rather long to build.) Makarius

[isabelle-dev] Unicode tokens and Isabelle fonts

2009-07-29 Thread Makarius
/ Their struggle probably shows how difficult mathematical font design actually is. Or maybe these guys are just clueless? Makarius

[isabelle-dev] Unicode tokens and Isabelle fonts

2009-07-29 Thread Makarius
On Wed, 29 Jul 2009, Alexander Krauss wrote: Makarius wrote: I am still hoping that the STIX project will deliver something after all these years, see http://www.aip.org/stixfonts/ I like the website: The target date for final release of this production version is two months ago

[isabelle-dev] Unicode tokens and Isabelle fonts

2009-07-29 Thread Makarius
-- seems to be part of some Fx stuff coming a bit later. In the mean time we have our own problems of getting robust Isabelle/Scala integration, with all the gory details done right, so that in the end there will be a usable system. Makarius

[isabelle-dev] Isabelle2009 fails to handle interrupts

2009-08-27 Thread Makarius
combinators will do it properly. Such misinterpreted interrupts might cause strange behaviour, but editor/toplevel state synchronization should not be lost. Makarius

[isabelle-dev] x-symbols

2009-09-03 Thread Makarius
-English keyboard: the alt-graph key is remapped by default, but something like this will help: (custom-set-variables '(ns-alternate-modifier 'none)) Makarius

[isabelle-dev] HOL FAILED

2009-10-01 Thread Makarius
by giving official changeset ids. The repository version is not a defined thing, and can change every minute. Makarius

[isabelle-dev] Explicit behaviour of apply(auto) ?

2009-10-02 Thread Makarius
test If you open the tree folds of HOL you will see a list of theorems -- the graph view is not so nice in this case. Makarius

[isabelle-dev] Isabelle release

2009-10-16 Thread Makarius
longer and longer as the system gets more complex. Now is the time to finish things and put them into a state for end-users out there. If there are still major things waiting in your pipeline, please say so. Makarius

[isabelle-dev] Getting Nitpick to run on your repository

2009-10-28 Thread Makarius
their own components in $ISABELLE_HOME_USER/etc/components, without having to edit central defaults. Makarius

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-12 Thread Makarius
anymore.) Makarius

[isabelle-dev] Isabelle/HOL axiom iff is redundant

2009-11-12 Thread Makarius
. Makarius

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-12 Thread Makarius
files.). Makarius

[isabelle-dev] Isabelle/HOL axiom ext is redundant

2009-11-13 Thread Makarius
, and the use of it by Isar, facilitated the genericity natural deduction-style reasoning. Generic proof tools can be written that work across logics. Makarius, if I understood correctly, was saying that these meta-level logical mechanisms have a utility even when just within one logic, but I

[isabelle-dev] Error message Failed to prepare dependency graph

2009-11-17 Thread Makarius
On Tue, 17 Nov 2009, Tjark Weber wrote: On Tue, 2009-11-17 at 15:18 +0100, Makarius wrote: A repository clone is not a proper distribution, and various parts are missing. The Admin/build script helps to fill these gaps, notably Admin/build browser Clemens used to maintain a web page

[isabelle-dev] Isabelle release

2009-11-18 Thread Makarius
On Fri, 16 Oct 2009, Makarius wrote: Dear Isabelle contributors, we need to approach the next official Isabelle release. The basic plan is to get things done this fall, which means there are only 2-3 weeks left for substantial changes. After that there will be a few more weeks

[isabelle-dev] Isabelle release snapshot

2009-11-25 Thread Makarius
of the official AFP release for Isabelle2009-1 that happens in parallel. Makarius

[isabelle-dev] UPDATE: Isabelle2009-1 test release

2009-11-27 Thread Makarius
to run without further ado. Makarius

[isabelle-dev] UPDATE: Isabelle2009-1 test release

2009-11-30 Thread Makarius
omissions. Makarius

[isabelle-dev] Typing problem in autogenerated axiom

2009-12-02 Thread Makarius
that would not be possible in Coq, for example. Makarius

[isabelle-dev] Isabelle2009-1 test release -- final call

2009-12-02 Thread Makarius
will probably produce the official Isabelle2009-1 snapshot tomorrow. Makarius

[isabelle-dev] Sledgehammer renaming

2010-01-13 Thread Makarius
. There seem to be several things intermingled, and many surprises will show up when trying to sort things out. Larry is probably closest to understanding the general outline. Also note that the ATP linkup is particularly tricky, because there are no formalized regression tests. Makarius

[isabelle-dev] Sledgehammer renaming

2010-01-13 Thread Makarius
. This state has not yet been achieved for nitpick, where Jasmin *is* fully responsible right now. Makarius

[isabelle-dev] Sledgehammer renaming

2010-01-14 Thread Makarius
On Thu, 14 Jan 2010, Alexander Krauss wrote: Makarius wrote: On Wed, 13 Jan 2010, Jasmin Blanchette wrote: 2. Generalize atp_manager.ML so that it can manage arbitrary assistants, which are tools that take a goal and produce a message -- not just ATPs -- and rename it HOL/Tools

[isabelle-dev] added 605 changesets with 1325 changes to 175 files

2010-01-16 Thread Makarius
On Sat, 16 Jan 2010, Alexander Krauss wrote: Hi Brian, added 605 changesets with 1325 changes to 175 files Wow! What just happened? Makarius merged in a long line of development concerning the interface from a previously separate repository: c13e168a8ae6 through e596a0b71f3c. BTW

[isabelle-dev] NEWS

2010-01-04 Thread Makarius
* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that proof terms are enabled unconditionally in the new HOL-Proofs image. Makarius

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-08 Thread Makarius
from your code. Makarius

[isabelle-dev] Method parsing, YXML and term construction.

2010-02-09 Thread Makarius
On Tue, 9 Feb 2010, Thomas Sewell wrote: Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem to be my friends. In fact, I sort of wish I'd known about them earlier. I remember in one of the record package proofs it was annoying me that I had to construct the types

[isabelle-dev] what's wrong with my system?

2010-03-01 Thread Makarius
not invoke the script directly: the browser already takes care of recompiling the required jars on demand. Makarius

[isabelle-dev] Pattern.match -- a minute

2010-03-03 Thread Makarius
example for now, you can use Logic.varify (although that does not work in general local situations, where parts are fixed and parts are arbitrary). Makarius

[isabelle-dev] Sane Mercurial history

2010-03-03 Thread Makarius
On Wed, 3 Mar 2010, Brian Huffman wrote: On Wed, Mar 3, 2010 at 8:54 AM, Makarius makarius at sketis.net wrote: * For longer projects the timespan of staying in splendid isolation is limited to 1-3 days (3 is already quite long, and personally I usually try to stay within the 0.5-1.5

[isabelle-dev] NEWS

2010-03-13 Thread Makarius
* 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)

Re: [isabelle-dev] Function package produces duplicate rewrite rule warnings

2010-05-05 Thread Makarius
. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

  1   2   3   4   5   6   7   8   9   10   >