[isabelle-dev] NEWS: session profiling

*** System *** * System option "profiling" specifies the mode for global ML profiling in "isabelle build". Possible values are "time", "allocations". This refers to Isabelle/b00508facb4f and 3d5e7719e878, which provides an updated "isabelle profiling_report" tool (that is not in the NEWS,

[isabelle-dev] NEWS: SSH and Mercurial support in Isabelle/Scala

*** System *** * Isabelle/Scala: the SSH module supports ssh and sftp connections, for remote command-execution and file-system access. This resembles operations from module File and Isabelle_System to some extent. Note that Path specifications need to be resolved remotely via ssh.remote_path

[isabelle-dev] NEWS: isabelle build performance tuning

*** System *** * The command-line tool "isabelle build" supports option -N for cyclic shuffling of NUMA CPU nodes. This may help performance tuning on Linux servers with separate CPU/memory modules. * The system option "threads" (for the size of the Isabelle/ML thread farm) is also passed to the

Re: [isabelle-dev] NEWS: new proof method "argo"

Hi Makarius, Compared to „argo“ the „smt“ method is more powerful since it supports quantifiers as well as linear natural and integer arithmetic. For the moment, argo is not capable of proving problems that require both equality reasoning and linear real arithmetic. This combination of

Re: [isabelle-dev] NEWS: new proof method "argo"

On 29/09/16 21:44, Sascha Boehme wrote: > *** HOL *** > > * New proof method "argo" using the built-in Argo solver based on SMT > technology. > The method can be used to prove goals of quantifier-free propositional logic, > goals based on a combination of quantifier-free propositional logic with

[isabelle-dev] NEWS: syntax for unique existence quantifier

*** HOL *** * The unique existence quantifier no longer provides 'binder' syntax, but uses syntax translations (as for bounded unique existence). Thus iterated quantification ∃!x y. P x y with its slightly confusing sequential meaning ∃!x. ∃!y. P x y is no longer possible. Instead, pattern

[isabelle-dev] NEWS: abbrevs and symbols dockable

*** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window "Symbols" also provides access to 'abbrevs' from the outer syntax of the current theory buffer. This provides clickable syntax templates, including entries with empty abbrevs name (which are inaccessible via keyboard completion). *

[isabelle-dev] NEWS: system option "checkpoint"

*** System *** * System option "checkpoint" helps to fine-tune the global heap space management of isabelle build. This is relevant for big sessions that may exhaust the small 32-bit address space of the ML process (which is used by default). This refers to Isabelle/b24d0e53dd03 (for

[isabelle-dev] NEWS: unfold_abs_def

*** General *** * The command 'unfolding' and proof method "unfold" include a second stage where given equations are passed through the attribute "abs_def" before rewriting. This ensures that definitions are fully expanded, regardless of the actual parameters that are provided. Rare

[isabelle-dev] NEWS: isabelle.keymap-merge

*** Prover IDE -- Isabelle/Scala/jEdit *** * Action "isabelle.keymap-merge" asks the user to resolve pending Isabelle keymap changes that are in conflict with the current jEdit keymap; non-conflicting changes are always applied implicitly. This action is automatically invoked on Isabelle/jEdit

[isabelle-dev] NEWS: split!

* Splitter in simp, auto and friends: - The syntax "split add" has been discontinued, use plain "split". - For situations with many conditional or case expressions, there is an alternative splitting strategy that can be much faster. It is selected by writing "split!" instead of "split". It

Re: [isabelle-dev] NEWS: proof outline with cases

On 08/08/16 10:52, Andreas Lochbihler wrote: > sometimes quotes are needed around the case name (e.g., if it is a > keyword like "try" or "oracle", or if it is a case of an induction rule > by the function package for an equation which has been split up by the > sequential option, i.e., 3_1 and

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

On 08/08/16 17:09, Andreas Lochbihler wrote: > > Additionally, you could declare bundles > with the existing notation > > "(f has_integral x) s" > > for both of them (like is nowadays done for the Lifting package syntax). > Then, you can locally include the notation for the desired integral

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

Hi Johannes, You could define the syntax for has_integral to be literally "(f Bochner.has_integral x) s" and similarly for the other. Additionally, you could declare bundles with the existing notation "(f has_integral x) s" for both of them (like is nowadays done for the Lifting

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

Am Montag, den 08.08.2016, 15:03 +0100 schrieb Lawrence Paulson: > Thank you for making this change! > > > > > My idea would be to rename both integrals into something like: > >   has_bc_integral, bc_integrable, bc_integral, > >   has_hk_integral, hk_integrable, hk_integral > > and consequently

Re: [isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

Thank you for making this change! > My idea would be to rename both integrals into something like: > has_bc_integral, bc_integrable, bc_integral, > has_hk_integral, hk_integrable, hk_integral > and consequently rename the integral theorems. I would greatly prefer renaming the relevant

[isabelle-dev] NEWS: Rename HOL-Multivariate_Analysis to HOL-Analysis and move measure theory from HOL-Probability to HOL-Analysis

* Renamed session HOL-Multivariate_Analysis to HOL-Analysis. * Moved measure theory from HOL-Probability to HOL-Analysis. When importing HOL-Analysis some theorems need additional name spaces prefixes due to name clashes. INCOMPATIBILITY. The incompatibility is obviously due to the renaming,

Re: [isabelle-dev] NEWS: proof outline with cases

Hi Makarius, Just a quick feedback on the proof outlines: they are great! But sometimes quotes are needed around the case name (e.g., if it is a keyword like "try" or "oracle", or if it is a case of an induction rule by the function package for an equation which has been split up by the

[isabelle-dev] NEWS: more PIDE structure parsing

*** Prover IDE -- Isabelle/Scala/jEdit *** * Isabelle/ML and Standard ML files are presented in Sidekick with the tree structure of section headings: this special comment format is described in "implementation" chapter 0, e.g. (*** section ***). * Refined folding mode "isabelle" based on Isar

[isabelle-dev] NEWS: abbrevs within theory header

*** Prover IDE -- Isabelle/Scala/jEdit *** * Additional abbreviations for syntactic completion may be specified within the theory header as 'abbrevs', in addition to global $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as before. The theory syntax for 'keywords' has been

Re: [isabelle-dev] NEWS: Primes

Yes, that might be a good idea. On 27/07/16 11:24, Tobias Nipkow wrote: Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization"

Re: [isabelle-dev] NEWS: Primes

Naming: can't we drop "is_"? Tobias On 27/07/2016 10:46, Manuel Eberl wrote: *** HOL *** * Number_Theory: algebraic foundation for primes: Introduction of predicates "is_prime", "irreducible", a "prime_factorization" function, the "factorial_ring" typeclass with instance proofs for nat, int,

[isabelle-dev] NEWS:

*** Prover IDE -- Isabelle/Scala/jEdit *** * Completion templates for commands involving "begin ... end" blocks, e.g. 'context', 'notepad'. This refers to Isabelle/0f39f59317c1. It can be seen as part of the standardized indenation policy, although only line breaks without extra indentation are

[isabelle-dev] NEWS: Proof methods "simp" and "simp_all" in Pure

*** General *** * Pure provides basic versions of proof methods "simp" and "simp_all" that only know about meta-equality (==). Potential INCOMPATIBILITY in theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order is relevant to avoid confusion of Pure.simp vs. HOL.simp. This

[isabelle-dev] NEWS: Proof method "use" in Pure

*** Isar *** * Proof method "use" allows to modify the main facts of a given method expression, e.g. (use facts in simp) (use facts in ‹simp add: ...›) This refers to Isabelle/59eff6e56d81. Before, the proof method "use" was part of Eisbach, which is still not in Pure because of its

[isabelle-dev] NEWS: proof outline with cases

*** Prover IDE -- Isabelle/Scala/jEdit *** * Command 'proof' provides information about proof outline with cases, e.g. for proof methods "cases", "induct", "goal_cases". This refers to Isabelle/6c46a1e786da. The main functionality is in Isabelle/9f8d06f23c09, which also demonstrates how to do

Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

On 15/07/16 11:49, Lawrence Paulson wrote: > It’s great, but can I pester you about my pet wish? It would be some sort of > “auto-complete” e.g. I type “proof (cases blah)” and somehow automatically > the full “case True show … next case False show … qed” skeleton could be > generated? The same

Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

This is another update according (presently at Isabelle/2033a3960c36): * Syntactic indentation according to Isabelle outer syntax. Action "indent-lines" (shortcut C+i) indents the current line according to command keywords and some command substructure. Action "isabelle.newline" (shortcut ENTER)

[isabelle-dev] NEWS: refined folding mode "isabelle"

*** Prover IDE -- Isabelle/Scala/jEdit *** * Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed' are treated as delimiters for fold structure. This refers to Isabelle/f10feaa9b14a. Makarius ___ isabelle-dev mailing list

Re: [isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

This is the updated situation according to Isabelle/019856db2bb6: *** Prover IDE -- Isabelle/Scala/jEdit *** * Improved support for indentation according to Isabelle outer syntax. Action "indent-lines" (shortcut C+i) indents the current line according to command keywords and some command

[isabelle-dev] NEWS: Indentation according to Isabelle outer syntax

*** Prover IDE -- Isabelle/Scala/jEdit *** * Indentation according to Isabelle outer syntax, cf. action "indent-lines" (shortcut C+i). This refers to Isabelle/52349e41d5dc. It is only the second round of refinement, beyond direct imitation of the old proof-indent.el from Proof General (see

[isabelle-dev] NEWS

* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying equations in functional programming style: variables present on the left-hand but not on the righ-hand side are replaced by underscores. See the tutorial "LaTeX Sugar for Isabelle Documents". Tobias smime.p7s Description:

[isabelle-dev] NEWS: "blast" is more robust

* Proof method "blast" is more robust wrt. corner cases of Pure statements without object-logic judgment. This refers to Isabelle/8bbd325e89e6, the relevant changes are by Larry (9a2377b96ffd, d2d26ff708d7). Makarius ___ isabelle-dev mailing

[isabelle-dev] NEWS: literal facts

* The defining position of a literal fact ‹prop› is maintained more carefully, and made accessible as hyperlink in the Prover IDE. * Commands 'finally' and 'ultimately' used to expose the result as literal fact: this accidental behaviour has been discontinued. Rare INCOMPATIBILITY, use more

[isabelle-dev] NEWS: bundle target and unbundle command

*** General *** * Command 'bundle' provides a local theory target to define a bundle from the body of specification commands (such as 'declare', 'declaration', 'notation', 'lemmas', 'lemma'). For example: bundle foo begin declare a [simp] declare b [intro] end * Command 'unbundle' is like

Re: [isabelle-dev] NEWS: method facts

On 09/06/16 16:25, Joachim Breitner wrote: > > But while I like "using" inside an proof, it does not please my sense > of aesthetic to have such a command before the initial "proof" command. Such initial 'using' is sometimes indeed awkward, but there is in general nothing wrong with it. BTW,

Re: [isabelle-dev] NEWS: method facts

Dear Markarius, Am Donnerstag, den 09.06.2016, 15:58 +0200 schrieb Makarius: > > [..] Turning 'using' into "use" is a downgrade of proof command into proof > method. This is occasionally useful, like e.g. using attribute > expressions instead of proof methods, but not something I would do all >

Re: [isabelle-dev] NEWS: method facts

Hi, Am Mittwoch, den 08.06.2016, 19:46 +0200 schrieb Makarius: > There are further possibilities for "use", e.g. to eliminate > auxiliary > "-" or "insert" steps, notably: > >   qed (insert a, auto)  ~>  qed (use a in auto) does this mean that the old idiom of lemma foo:   assumes

[isabelle-dev] NEWS: method facts

*** Isar *** * Proof methods may refer to the main facts via the dynamic fact "method_facts". This is particularly useful for Eisbach method definitions. * Eisbach provides method "use" to modify the main facts of a given method expression, e.g. (use facts in simp) (use facts in ‹simp add:

[isabelle-dev] NEWS: isabelle.select-entity

*** Prover IDE -- Isabelle/Scala/jEdit *** * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all occurences of the formal entity at the caret position. This facilitates systematic renaming. This refers to Isabelle/48bc9045866e. As usual, new keyboard shortcuts need to be provided

[isabelle-dev] NEWS: clarified Integer.gcd and Integer.lcm

*** ML *** * Integer.gcd and Integer.lcm use efficient operations from the Poly/ML (notably for big integers). Subtle change of semantics: Integer.gcd and Integer.lcm both normalize the sign, results are never negative. This coincides with the definitions in HOL/GCD.thy. INCOMPATIBILITY. This

Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

Very good! This is very convenient. On 01/06/16 21:42, Makarius wrote: *** ML *** * Structure Rat for rational numbers is now an integral part of Isabelle/ML, with special notation @int/nat or @int for numerals (an abbreviation for antiquotation @{Pure.rat argument}) and ML pretty printing.

Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

On 01/06/16 21:47, Lawrence Paulson wrote: > Doesn’t Poly/ML include an option to support GCDs (if not rationals) > efficiently? Do you mean PolyML.IntInf.gcd and PolyML.IntInf.lcm? That is already used (da38571dd5bd). These operations normally use GNU MP, but on Mac OS X only the old builtin

Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

On 01/06/16 21:58, Florian Haftmann wrote: > > One could regard the dedicated literal syntax for rationals a little bit > oversophisticated; maybe an infix // for Rat.make would serve better. > Or we could A matter of personal taste, though. There is a delicate point here: our antiquotation

Re: [isabelle-dev] NEWS: Rat in Isabelle/ML

> * Structure Rat for rational numbers is now an integral part of > Isabelle/ML, with special notation @int/nat or @int for numerals (an > abbreviation for antiquotation @{Pure.rat argument}) and ML pretty > printing. Standard operations on type Rat.rat are provided via ad-hoc > overloading of + -

[isabelle-dev] NEWS: Rat in Isabelle/ML

*** ML *** * Structure Rat for rational numbers is now an integral part of Isabelle/ML, with special notation @int/nat or @int for numerals (an abbreviation for antiquotation @{Pure.rat argument}) and ML pretty printing. Standard operations on type Rat.rat are provided via ad-hoc overloading of +

[isabelle-dev] NEWS

Code generator: config option "code_timinger" triggers measurements of different phases of code generation. See src/HOL/ex/Code_Timing.thy for examples. This enables a canonical way to examine performance of generated code and corresponding computations on different levels. In the process of

[isabelle-dev] NEWS: theorem eigen context

*** Isar *** * Toplevel theorem statements support eigen-context notation with 'if' / 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the traditional long statement form (in prefix). Local premises are called "that" or "assms", respectively. Empty premises are *not* bound in the

[isabelle-dev] NEWS: cartouches

*** General *** * Embedded content (e.g. the inner syntax of types, terms, props) may be delimited uniformly via cartouches. This works better than old-fashioned quotes when sub-languages are nested. *** Prover IDE -- Isabelle/Scala/jEdit *** * Cartouche abbreviations work both for " and ` to

Re: [isabelle-dev] NEWS: process management (summary and update)

On 20/03/16 06:41, Lars Noschinski wrote: > On 11.03.2016 18:37, Makarius wrote: >> * The executable "isabelle_process" has been discontinued. Tools and >> prover front-ends should use ML_Process or Isabelle_Process in >> Isabelle/Scala. INCOMPATIBILITY. >> >> * New command-line tool "isabelle

Re: [isabelle-dev] NEWS: command 'define'

Very nice! Am 25.04.2016 um 21:57 schrieb Makarius: > *** Isar *** > > * Command 'define' introduces a local (non-polymorphic) definition, with > optional abstraction over local parameters. The syntax resembles > 'definition' and 'obtain'. It fits better into the Isar language than > old 'def',

[isabelle-dev] NEWS: command 'define'

*** Isar *** * Command 'define' introduces a local (non-polymorphic) definition, with optional abstraction over local parameters. The syntax resembles 'definition' and 'obtain'. It fits better into the Isar language than old 'def', which is now a legacy feature. This refers to

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

Hi Dmitriy, Makarius, Dmitriy wrote: > At first I was a bit surprised to see the first occurrence of list, Nil, and > Cons in blue in the following datatype definitions. > > datatype 'a list = Nil | Cons 'a "'a list” > > But I guess, it makes sense to indicate that this is a new thing being

Re: [isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap

*** Prover IDE -- Isabelle/Scala/jEdit *** * IDE support for the Isabelle/Pure bootstrap process, with the following independent stages: src/Pure/ROOT0.ML src/Pure/ROOT.ML src/Pure/Pure.thy src/Pure/ML_Bootstrap.thy The ML ROOT files act like quasi-theories in the context of theory

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

On Tue, 19 Apr 2016, Dmitriy Traytel wrote: At first I was a bit surprised to see the first occurrence of list, Nil, and Cons in blue in the following datatype definitions. datatype 'a list = Nil | Cons 'a "'a list” But I guess, it makes sense to indicate that this is a new thing being

Re: [isabelle-dev] NEWS: Highlighting of entity def/ref positions

Hi Makarius, this is nice. At first I was a bit surprised to see the first occurrence of list, Nil, and Cons in blue in the following datatype definitions. datatype 'a list = Nil | Cons 'a "'a list” But I guess, it makes sense to indicate that this is a new thing being defined. The question

[isabelle-dev] NEWS: Highlighting of entity def/ref positions

*** Prover IDE -- Isabelle/Scala/jEdit *** * Highlighting of entity def/ref positions wrt. cursor. This refers to Isabelle/15e6ae52e91a, where it is pushed through most definitional packages already. Name bindings need to be treated carefully with their position information, but it also

Re: [isabelle-dev] NEWS: HOL-Probability -- type of emeasure and nn_integral was changed from ereal to ennreal

Argh, the change to the AFP broke the entire build by accidentally removing `Ergodic_Theory/document/root.tex`. I don't know how this happened. It is fixed now. Sorry for the inconvenience. - Johannes Am Donnerstag, den 14.04.2016, 15:57 +0200 schrieb Johannes Hölzl: > In HOL-Probability the

Re: [isabelle-dev] NEWS: type-inference for object-logic

On Tue, 12 Apr 2016, Peter Lammich wrote: so we're not going to see the annoying "... not of sort 'type'" error any more, which used to occur occasionally in Isabelle/HOL developments!? Yes, but old tools may get broken, if slightly more general types are expected. E.g. see the record

Re: [isabelle-dev] NEWS: type-inference for object-logic

Nice one, so we're not going to see the annoying "... not of sort 'type'" error any more, which used to occur occasionally in Isabelle/HOL developments!? -- Peter On Di, 2016-04-12 at 16:46 +0200, Makarius wrote: > *** General *** > > * Type-inference improves sorts of newly introduced type

[isabelle-dev] NEWS: type-inference for object-logic

*** General *** * Type-inference improves sorts of newly introduced type variables for the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). Thus terms like "f x" or "⋀x. P x" without any further syntactic context produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare

Re: [isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap

On Thu, 7 Apr 2016, Makarius wrote: *** Prover IDE -- Isabelle/Scala/jEdit *** * IDE support for the Isabelle/Pure bootstrap process. After further refinements (e.g. see current Isabelle/79f41fbdf74a), the Pure IDE bootstrap works even more smoothly. In particular it can be combined with

Re: [isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap

On Thu, 7 Apr 2016, Makarius wrote: Maybe some other big applications of Poly/ML should be made PIDE-compliant as well, e.g. HOL4 or even Poly/ML itself. Or maybe even this one: https://bitbucket.org/lcpaulson/metitarski Makarius ___

[isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap

*** Prover IDE -- Isabelle/Scala/jEdit *** * IDE support for the Isabelle/Pure bootstrap process. The file src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a theory body in the context of theory ML_Bootstrap. This allows continuous checking of ML files as usual, but the result is

[isabelle-dev] NEWS: ISABELLE_TOOL_JAVA_OPTIONS

*** System *** * Many Isabelle tools that require a Java runtime system refer to the settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64, depending on the underlying platform. The settings for "isabelle build" ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have

Re: [isabelle-dev] NEWS: mixfix annotations and Unicode

On Sat, 2 Apr 2016, Makarius wrote: I am considering to force Isabelle/jEdit text into Unicode non-conformance, to make logical sense. Or we could disallow Unicode notation altogether -- it is hardly ever used, apart from some exotic demos. A similar problem will show up again, if/when

[isabelle-dev] NEWS: mixfix annotations and Unicode

*** General *** * Mixfix annotations support general block properties, with syntax "(‹x=a y=b z …›". Notable property names are "indent", "consistent", "unbreakable", "markup". The existing notation "(DIGITS" is equivalent to "(‹indent=DIGITS›". The former notation "(00" for unbreakable blocks

Re: [isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

> On Sat, 12 Mar 2016, Florian Haftmann wrote: > >> * A type of infinitely many characters could serve a model for unicode >> characters. > > Unicode has only finitely many code points. Presently, 21 bits are > sufficient to encode that. > > Does it make sense to have a char type with

Re: [isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

> On Sat, 12 Mar 2016, Florian Haftmann wrote: > >> * Simplifying the character syntax further. e.g. getting rid of CHR vs. >> CHAR. > > That should be trivial: > > syntax > "_Char" :: "str_position ⇒ char" ("CHR _") > "_Char_ord" :: "num_const ⇒ char" ("CHR _") For the record: this

Re: [isabelle-dev] NEWS: Poly/ML heaps follow hierarchy of sessions

On Thu, 17 Mar 2016, Lawrence Paulson wrote: This is a great achievement! And disk space is still important, especially on modern devices with SSDs. The main work is by David Matthews, and it happened over the past few years. Without SML/NJ and old Poly/ML versions hindering us, we can now

Re: [isabelle-dev] NEWS: process management (summary and update)

On 11.03.2016 18:37, Makarius wrote: > * The executable "isabelle_process" has been discontinued. Tools and > prover front-ends should use ML_Process or Isabelle_Process in > Isabelle/Scala. INCOMPATIBILITY. > > * New command-line tool "isabelle process" supports ML evaluation of > literal

Re: [isabelle-dev] NEWS:

This is a great achievement! And disk space is still important, especially on modern devices with SSDs. My machine has only 20 GB to spare. Larry > On 16 Mar 2016, at 22:33, Makarius wrote: > > *** System *** > > * Poly/ML heaps now follow the hierarchy of sessions, and

Re: [isabelle-dev] NEWS: Poly/ML heaps follow hierarchy of sessions

On Wed, 16 Mar 2016, Makarius wrote: *** System *** * Poly/ML heaps now follow the hierarchy of sessions, and thus require much less disk space. x86-linux build -a -b -d '$AFP': 96GB ~> 8.3GB (without JinjaThreads) Here are some more numbers, using Isabelle/a2351f82bc48 and

[isabelle-dev] NEWS:

*** System *** * Poly/ML heaps now follow the hierarchy of sessions, and thus require much less disk space. This refers to Isabelle/c36a4495ba5f. Instead of a quick patch, it is the result of profound reforms of how heaps and processes are managed. This has become feasible after the

Re: [isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

On Sat, 12 Mar 2016, Florian Haftmann wrote: * All other characters are represented as »Char n« BTW, these Unicode guillemets cause problems in the NEWS file, which is subject to standard Isabelle symbol interpretation. I've changed that in a2351f82bc48. Another Unicode accident (by

Re: [isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

On Sat, 12 Mar 2016, Florian Haftmann wrote: * A type of infinitely many characters could serve a model for unicode characters. Unicode has only finitely many code points. Presently, 21 bits are sufficient to encode that. Does it make sense to have a char type with somewhat "unspecified"

[isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

- Logical representation: * 0 is instantiated to the ASCII zero character. * All other characters are represented as »Char n« with n being a raw numeral expression less than 256. * Expressions of the form »Char n« with n greater than 255 are non-canonical. - Printing and parsing: *

[isabelle-dev] NEWS: process management (summary and update)

*** System *** * The Isabelle system environment always ensures that the main executables are found within the shell search $PATH: "isabelle" and "isabelle_scala_script". * The Isabelle ML process is now managed directly by Isabelle/Scala, and shell scripts merely provide optional command-line

Re: [isabelle-dev] NEWS: isabelle_process and isabelle console

On Sat, 5 Mar 2016, Makarius wrote: The discontinuation of SML/NJ and old Poly/ML versions means that we can now use more up-to-date ways to manage the poly process. A bit more is coming later. More has happened in various changes leading to Isabelle/739a84403864: isabelle_process is based

Re: [isabelle-dev] NEWS: Local_Theory.restore versus Local_Theory.reset

> On 05 Mar 2016, at 23:11, Makarius wrote: > > *** ML *** > > * Local_Theory.restore has been renamed to Local_Theory.reset to > emphasize its disruptive impact on the cumulative context, notably the > scope of 'private' or 'qualified' names. Note that Local_Theory.reset

Re: [isabelle-dev] NEWS: HOL notation

We might also consider the negations of \in, \subseteq, \subset and even perhaps < and > Larry > On 5 Mar 2016, at 22:19, Makarius wrote: > > * New abbreviations for negated existence (but not bounded existence): > > ∄x. P x ≡ ¬ (∃x. P x) > ∄!x. P x ≡ ¬ (∃!x. P x)

[isabelle-dev] NEWS: structure Timeout

*** ML *** * Structure TimeLimit (originally from the SML/NJ library) has been replaced by structure Timeout, with slightly different signature. INCOMPATIBILITY. This refers to Isabelle/a564458f94db. Note that the exception Timeout.TIMEOUT is now more informative: it contains the actual time

[isabelle-dev] NEWS: isabelle_process and isabelle console

*** System *** * Command-line tool "isabelle_process" no longer supports writable heap images. INCOMPATIBILITY in exotic situations where "isabelle build" cannot be used: the structure ML_Heap provides operations to save the ML heap under program control. * Command-line tool "isabelle_process"

[isabelle-dev] NEWS: Local_Theory.restore versus Local_Theory.reset

*** ML *** * Local_Theory.restore has been renamed to Local_Theory.reset to emphasize its disruptive impact on the cumulative context, notably the scope of 'private' or 'qualified' names. Note that Local_Theory.reset is only appropriate when targets are managed, e.g. starting from a global

Re: [isabelle-dev] NEWS: support for ML_exception_debugger

The matter turned out quite simple: a literal type constructor name has to be adjusted: > diff -r eef7af6af2ce thys/Native_Word/Uint32.thy > --- a/thys/Native_Word/Uint32.thy Thu Mar 03 08:24:04 2016 +0100 > +++ b/thys/Native_Word/Uint32.thy Thu Mar 03 13:13:04 2016 +0100 > @@ -300,7

[isabelle-dev] NEWS: support for ML_exception_debugger

*** ML *** * Option ML_exception_debugger controls detailed exception trace via the Poly/ML debugger. Relevant ML modules need to be compiled beforehand with ML_file_debug, or with ML_file and option ML_debugger enabled. Note debugger information requires consirable time and space: main

[isabelle-dev] NEWS

* Multiset membership is now expressed using set_mset rather than count. ASCII infix syntax ":#" has been discontinued. - Expressions "count M a > 0" and similar simplify to membership by default. - Converting between "count M a = 0" and non-membership happens using equations

Re: [isabelle-dev] NEWS

On Thu, 25 Feb 2016, Lawrence Paulson wrote: More complex analysis including Cauchy's inequality, Liouville theorem, open mapping theorem, maximum modulus principle, Schwarz Lemma. (See theory Conformal_Mappings.) For the historical record: this refers to Isabelle/86f27b264d3d.

[isabelle-dev] NEWS

More complex analysis including Cauchy's inequality, Liouville theorem, open mapping theorem, maximum modulus principle, Schwarz Lemma. (See theory Conformal_Mappings.) Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] NEWS: \

*** Isar *** * Command '\' is an alias for 'sorry', with different typesetting. E.g. to produce proof holes in examples and documentation. This refers to Isabelle/5e5a881ebc12. It means that manuals, tutorials, slides etc. may be written more easily, without odd conditionals in LaTeX for the

[isabelle-dev] NEWS: better resource usage on all platforms

This refers to the NEWS update in adcaaf6c9910. In the past few months there have been many changes on both the ML and Scala side to make more of available resources, and to avoid demanding too much of them. In the coming weeks it is important to keep a keen eye on how it works in practice.

Re: [isabelle-dev] NEWS: print mode ASCII vs. xsymbols

On Tue, 29 Dec 2015, Makarius wrote: This refers to Isabelle/0a5dd617a88c. A bit more changes may follow later. Here is an updated summary according to Isabelle2016-RC0, with further notes at the bottom: *** General *** * Former "xsymbols" syntax with Isabelle symbols is used by

[isabelle-dev] NEWS: print mode ASCII vs. xsymbols

*** General *** * Former "xsymbols" syntax with Isabelle symbols is used by default, without any special print mode. Important ASCII replacement syntax remains available under print mode "ASCII", but less important syntax has been removed (see below). *** HOL *** * Some old and rarely used

Re: [isabelle-dev] NEWS: State panel

On Tue, 10 Nov 2015, Fabian Immler wrote: I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you

[isabelle-dev] NEWS: fundamental PIDE GUI changes

This is a summary of some fundamental changes in the dynamics PIDE edits and GUI updates, according to current Isabelle/ba051060d46b: * Improved scheduling for urgent print tasks (e.g. command state output, interactive queries) wrt. long-running background tasks. * The State panel manages

Re: [isabelle-dev] NEWS: State panel

On Tue, 10 Nov 2015, Mathias Fleury wrote: As a side question, is there a way to have two different panels docked at bottom open at the same time (i.e. splitting the bottom area into two parts and have two different panels in each)? According to current Isabelle/ba051060d46b, the default

Re: [isabelle-dev] NEWS: State panel

Hello Makarius, this might be intended, but in Isabelle/a99125aa964f from this morning the errors and warnings still goes to the output panel, which means that both panel have to be opened at the same time. Could you give us some insights about your workflow (for theorem proving) with the

Re: [isabelle-dev] NEWS: State panel

> On 9 Nov 2015, at 9:41 pm, Makarius wrote: > > * The State panel manages explicit proof state output, with jEdit action > "isabelle.update-state" (shortcut S+ENTER) to trigger update according > to cursor position. > > * The Output panel no longer shows proof state output

Re: [isabelle-dev] NEWS: State panel

Hi Makarius, I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you trigger output on the

Re: [isabelle-dev] NEWS: State panel

On 10/11/2015 14:20, Gerwin Klein wrote: On 9 Nov 2015, at 9:41 pm, Makarius wrote: * The State panel manages explicit proof state output, with jEdit action "isabelle.update-state" (shortcut S+ENTER) to trigger update according to cursor position. * The Output panel no

<    1   2   3   4   5   6   7   8   >