Re: [isabelle-dev] proper use of error channel

2010-03-23 Thread Makarius
On Tue, 23 Mar 2010, Tobias Nipkow wrote: Makarius schrieb: A few hints on using the error function in Isabelle/ML properly. Shouldn't this go into some documentation for future reference? I have marked it as one of the items to go into the chapter 0 about Isabelle/ML of the Isabelle/Isar

[isabelle-dev] Isabelle/Scala on Scala 2.8.0 Beta 1

2010-03-30 Thread Makarius
6.8, which requires Scala 2.8. Makarius ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] fconv_rule

2007-07-03 Thread Makarius
Does anyboy remember why fconv_rule is called like this? After peeking into the HOL Light sources I've got the impression that this function is usually called conv_rule. (Conversions have become popular recently so it might be a good point to sort this out now.) Makarius

[isabelle-dev] HOL-NumberTheory runtime

2007-07-19 Thread Makarius
Does anybody know why the runtime of HOL-NumberTheory has doubled recently? (See http://isabelle.in.tum.de/devel/stats/at-poly.html) Makarius

[isabelle-dev] NEWS

2007-07-20 Thread Makarius
* Theory loader: be more serious about observing the static theory header specifications (including optional directories), but not the accidental file locations of previously successful loads. Potential INCOMPATIBILITY, may need to refine theory headers. * Theory loader: optional support for

[isabelle-dev] NEWS

2007-07-28 Thread Makarius
* Isar: command 'declaration' augments a local theory by generic declaration functions written in ML. This enables arbitrary content being added to the context, depending on a morphism that tells the difference of the original declaration context wrt. the application context encountered later on.

[isabelle-dev] NEWS

2007-07-31 Thread Makarius
* Configuration options are maintained within the theory or proof context (with name and type bool/int/string), providing a very simple interface to a poor-man's version of general context data. Tools may declare options in ML (e.g. using ConfigOption.int) and then refer to these values using

[isabelle-dev] fconv_rule

2007-07-03 Thread Makarius
Does anyboy remember why fconv_rule is called like this? After peeking into the HOL Light sources I've got the impression that this function is usually called conv_rule. (Conversions have become popular recently so it might be a good point to sort this out now.) Makarius

[isabelle-dev] NEWS

2007-08-09 Thread Makarius
* Theory loader: old-style ML proof scripts being *attached* to a thy file (with the same base name as the theory) are considered a legacy feature, which will disappear eventually. Even now, the theory loader no longer maintains dependencies on such files.

[isabelle-dev] NEWS

2007-08-12 Thread Makarius
* Syntax: the scope for resolving ambiguities via type-inference is now limited to individual terms, instead of whole simultaneous specifications as before. This greatly reduces the complexity of the syntax module and improves flexibility by separating parsing and type-checking. INCOMPATIBILITY:

[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] [polyml] Forthcoming 5.1 release (fwd)

2007-11-06 Thread Makarius
-- Forwarded message -- Date: Tue, 06 Nov 2007 08:56:38 + From: David Matthews david.matth...@prolingua.co.uk To: PolyML mailing list polyml at inf.ed.ac.uk Subject: [polyml] Forthcoming 5.1 release There has been quite a lot of work on Poly/ML over the last year and I'm

[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

2007-11-04 Thread Makarius
* System: run-polyml-5.1 now uses PolyML.SaveState instead of linked object-files (this is potentially more efficient). INCOMPATIBILITY, requires recent Poly/ML cvs version and recompilation of logic images.

[isabelle-dev] NEWS

2007-12-20 Thread Makarius
* Metis prover is now an order of magnitude faster, and also works with multithreading.

[isabelle-dev] NEWS

2008-01-06 Thread Makarius
* 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/makedist).

[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-25 Thread Makarius
* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs --- in accordance with Proof General 3.7, which prefers GNU emacs.

[isabelle-dev] token translations

2008-01-26 Thread Makarius
On Sat, 26 Jan 2008, Steven Obua wrote: Makarius wrote: This is because token translations are only used when printing terms, not when presenting theory sources. Yes, I noticed that. Is there any quick hack around it ? No way. Makarius

[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

2008-03-05 Thread Makarius
* Indexing of literal facts: be more serious about including only facts from the visible specification/proof context, but not the background context (locale etc.). Affects `prop` notation and method fact. INCOMPATIBILITY: need to name facts explicitly in rare situations.

[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] NEWS

2008-06-28 Thread Makarius
* Document preparation: antiquotation @{lemma} now imitates a regular terminal proof, demanding keyword 'by' and supporting the full method expression syntax. * ML antiquotations: block-structured compilation context indicated by \lbrace ... \rbrace; additional antiquotation forms: @{let

[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] Isabelle history via Mercurial

2008-07-03 Thread Makarius
of legacy features over time. Only the better-known git by Torvalds is a bit more cryptic, being targeted at kernel hackers, but his Google talk is quite interesting nonetheless. 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
*** System *** * Isabelle/lib/classes/Pure.jar provides basic support to integrate the Isabelle process into a JVM/Scala application. See Isabelle/lib/jedit/plugin for a minimal example. (The obsolete Java process wrapper has been discontinued.) * Status messages (with exact source position

[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] new isabelle interface

2008-08-25 Thread Makarius
if native windows stuff is run via Cygwin.) Our JVM/Scala layer will also hold up this Posix-ish view, e.g. Isabelle file names like ~/tmp/A.thy or $ISABELLE_HOME/src/HOL/List.thy will be handled as expected. 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] NEWS

2008-08-25 Thread Makarius
On Sat, 23 Aug 2008, Makarius wrote: * Homegrown Isabelle font with unicode layout, see Isabelle/lib/fonts. Further font experiments are available here: http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/isabelle-fonts/ A version of this material will show up in the Isabelle distribution

[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] Relation_Power.thy

2008-09-02 Thread Makarius
). The idea is to make the output the same as \caret, of course (with the disadvantage that you can't wave your mouse over a piece of paper). You can, if it is electronic paper like PDF or even DVI (using recent link-enabled xdvi, 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] NEWS

2008-09-02 Thread Makarius
* Generic Toplevel.add_hook interface allows to analyze the result of transactions (including failed ones). For example, see src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency output of transactions resulting in a new theory state.

[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] NEWS

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

[isabelle-dev] NEWS

2008-09-18 Thread Makarius
* ML bindings produced via Isar commands are stored within the Isar context (theory or proof). Consequently, commands like 'use' and 'ML' become thread-safe and work with undo as expected (concerning top-level bindings, not side-effects on global references). INCOMPATIBILITY, need to provide

[isabelle-dev] NEWS

2008-09-18 Thread Makarius
* Simplified ML oracle interface Thm.add_oracle promotes 'a - cterm to 'a - thm, while results are always tagged with an authentic oracle name. The Isar command 'oracle' is now polymorphic, no argument type is specified. INCOMPATIBILITY, need to simplify existing oracle code accordingly. Note

[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: SourceForge.net CVS Migration and Downtime Announcement]

2008-09-30 Thread Makarius
have another benefit, giving Isabelle developers some practice in working with the new environment. (Mercurial is much more powerful than CVS/SVN, and there is more potential to do things wrong for inexperienced users.) 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
. The struggle to get rid of legacy stuff will continue ... Makarius

[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] NEWS (update)

2008-11-30 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] 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] Isabelle on Mercurial

2008-12-03 Thread Makarius
routine merges, and clearly indicates so in the log entry. A non-trivial situation needs to be handled separately, with hand-written log entry as appropriate to the situation. In most cases the message should be just merged, unless a real semantic conflict was resolved. 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] segfault compiling

2009-01-05 Thread Makarius
, or even the cvs head. Poly/ML did not change yet after the 5.2.1 release, so trying just the version from http://isabelle.in.tum.de/polyml-5.2.1/ should be fine. Makarius

[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] Isabelle2009 release

2009-02-27 Thread Makarius
that is also user relevant should be entered there; if it is not user relevant, it is probably a condidate for deletion. Concerning the CONTRIBUTORS file: if you are too shy to add yourself, you can also tell me and I will do it. Makarius

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

2009-02-28 Thread Makarius
On Wed, 11 Feb 2009, Florian Haftmann wrote: Concerning the number of merges, it is just - as far as I know - an observation that in presence of parallel proofs less merges increase speed. But perhaps Makarius can tell further details regarding this. In principle you do not have to care

[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] A better policy for the typerep class

2009-02-28 Thread Makarius
on that idea altogether. Nonetheless, I could imagine to have at least infixes managed in a more systematic way, not just collections of grammar productions. Makarius

[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] hg

2009-03-05 Thread Makarius
diff.changed = white diff.trailingwhitespace = bold red_background Note that the less pager requires option -R (e.g. via env LESS) to interpret color codes properly. Makarius

[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] Strange phenomenon with presburger

2009-03-10 Thread Makarius
on to user-space tools. E.g. like this: lemma False == (!!uu m n x. P x -- Suc(2 *m) ~= 2 *n) apply (tactic {* Goal.norm_hhf_tac 1 *}) apply (tactic {* blast_tac HOL_cs 1 *}) done Makarius

[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] repos integrity

2009-06-19 Thread Makarius
. Makarius

  1   2   3   4   5   6   7   8   9   10   >