1.1 --- a/.hgtags Mon Jun 21 16:59:37 2010 +0200
1.2 +++ b/.hgtags Mon Jun 21 17:41:57 2010 +0200
1.3 @@ -25,5 +25,4 @@
1.4 fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005
1.5 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009
1.6 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
1.7 -935c75359742ccfd4abba0c33a440241e6ef2b1e isa2009-2-test0
1.8 -d1cdbc7524b619815236e8e2e61e36809ee2d338 isa2009-2-test1
1.9 +35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
2.1 --- a/Admin/CHECKLIST Mon Jun 21 16:59:37 2010 +0200
2.2 +++ b/Admin/CHECKLIST Mon Jun 21 17:41:57 2010 +0200
2.3 @@ -15,7 +15,7 @@
2.4
2.5 - Admin/update-keywords;
2.6
2.7 -- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS;
2.8 +- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
2.9
2.10 - diff NEWS wrt. last official release, which is read-only;
2.11
3.1 --- a/Admin/makebundle Mon Jun 21 16:59:37 2010 +0200
3.2 +++ b/Admin/makebundle Mon Jun 21 17:41:57 2010 +0200
3.3 @@ -66,7 +66,7 @@
3.4 HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz"
3.5 [ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE"
3.6 echo "heaps"
3.7 -tar -C "$ISABELLE_HOME" -x -z -f "$HEAPS_ARCHIVE"
3.8 +tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE"
3.9
3.10
3.11 BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz"
4.1 --- a/Admin/makedist Mon Jun 21 16:59:37 2010 +0200
4.2 +++ b/Admin/makedist Mon Jun 21 17:41:57 2010 +0200
4.3 @@ -4,7 +4,7 @@
4.4
4.5 ## global settings
4.6
4.7 -REPOS_NAME="isabelle"
4.8 +REPOS_NAME="isabelle-release"
4.9 REPOS="http://isabelle.in.tum.de/repos/${REPOS_NAME}"
4.10
4.11 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
4.12 @@ -145,6 +145,11 @@
4.13 rm -rf doc-src
4.14
4.15 mkdir -p contrib
4.16 +cat >contrib/README <<EOF
4.17 +This directory contains add-on components that contribute to the main
4.18 +Isabelle distribution. Separate licensing conditions apply, see each
4.19 +directory individually.
4.20 +EOF
4.21
4.22 cp doc/isabelle*.eps lib/logo
4.23
4.24 @@ -200,9 +205,8 @@
4.25 mv "$DISTNAME" "${DISTNAME}-old"
4.26 mkdir "$DISTNAME"
4.27
4.28 -mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
4.29 - "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
4.30 - "$DISTNAME"
4.31 +mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
4.32 + "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
4.33 mkdir "$DISTNAME/doc"
4.34 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
4.35
5.1 --- a/INSTALL Mon Jun 21 16:59:37 2010 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,87 +0,0 @@
5.4 -
5.5 -Isabelle installation notes
5.6 -===========================
5.7 -
5.8 -1) System installation
5.9 -----------------------
5.10 -
5.11 -The Isabelle distribution includes both complete sources and
5.12 -precompiled binary packages for common Unix-like platforms.
5.13 -
5.14 -
5.15 -Quick installation
5.16 -------------------
5.17 -
5.18 -Ready-to-go packages are provided for the ML compiler and runtime
5.19 -system, the Isabelle sources, and some major object-logics. A minimal
5.20 -site installation of Isabelle on Linux/x86 works like this:
5.21 -
5.22 - tar -C /usr/local -xzf Isabelle.tar.gz
5.23 - tar -C /usr/local -xzf polyml.tar.gz
5.24 - tar -C /usr/local -xzf HOL_x86-linux.tar.gz
5.25 -
5.26 -The install prefix given above may be changed as appropriate; there is
5.27 -no need to install into a system directory like /usr/local at all. By
5.28 -default the ML system (and other contributed packages) are expected in
5.29 -any of the following locations:
5.30 -
5.31 - 1) [ISABELLE_HOME]/contrib
5.32 - 2) [ISABELLE_HOME]/..
5.33 - 4) /usr/local
5.34 - 3) /usr/share
5.35 - 5) /opt
5.36 -
5.37 -This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
5.38 -
5.39 -The installation may be finished as follows:
5.40 -
5.41 - cd [ISABELLE_HOME]
5.42 - ./bin/isabelle install -p /usr/local/bin
5.43 -
5.44 -The install utility creates global references to the present Isabelle
5.45 -installation, enabling users to invoke the Isabelle executables
5.46 -without explicit path names. This is the only place where a static
5.47 -reference to [ISABELLE_HOME] is created; thus isabelle install has to
5.48 -be run again whenever the Isabelle distribution is moved later.
5.49 -
5.50 -
5.51 -Compiling logics
5.52 -----------------
5.53 -
5.54 -The Isabelle.tar.gz archive already contains all Isabelle sources (and
5.55 -documentation). Precompiled object-logics are provided for
5.56 -convenience.
5.57 -
5.58 -Assuming proper configuration of the underlying ML system
5.59 -(cf. Isabelle's etc/settings), further object-logics may be compiled
5.60 -like this:
5.61 -
5.62 - [ISABELLE_HOME]/build FOL
5.63 -
5.64 -Special object-logic targets may be specified as follows:
5.65 -
5.66 - [ISABELLE_HOME]/build -m HOL-Algebra HOL
5.67 -
5.68 -
5.69 -2) User installation
5.70 ---------------------
5.71 -
5.72 -Running the Isabelle binaries
5.73 ------------------------------
5.74 -
5.75 -Users may invoke the main Isabelle binaries (isabelle and
5.76 -isabelle-process) directly from their location within the distribution
5.77 -directory [ISABELLE_HOME] like this:
5.78 -
5.79 - [ISABELLE_HOME]/bin/isabelle tty -l HOL
5.80 -
5.81 -This starts an interactive Isabelle session within the current text
5.82 -terminal. [ISABELLE_HOME]/bin may be put into the shell's search
5.83 -PATH. An alternative is to create global references to the Isabelle
5.84 -executables as follows:
5.85 -
5.86 - [ISABELLE_HOME]/bin/isabelle install -p ~/bin
5.87 -
5.88 -Note that the site-wide Isabelle installation may already provide
5.89 -Isabelle executables in some global bin directory (such as
5.90 -/usr/local/bin).
6.1 --- a/NEWS Mon Jun 21 16:59:37 2010 +0200
6.2 +++ b/NEWS Mon Jun 21 17:41:57 2010 +0200
6.3 @@ -202,15 +202,15 @@
6.4 'quotient_definition' may be used for defining types and constants by
6.5 quotient constructions. An example is the type of integers created by
6.6 quotienting pairs of natural numbers:
6.7 -
6.8 +
6.9 fun
6.10 - intrel :: "(nat * nat) => (nat * nat) => bool"
6.11 + intrel :: "(nat * nat) => (nat * nat) => bool"
6.12 where
6.13 "intrel (x, y) (u, v) = (x + v = u + y)"
6.14
6.15 - quotient_type int = "nat × nat" / intrel
6.16 + quotient_type int = "nat * nat" / intrel
6.17 by (auto simp add: equivp_def expand_fun_eq)
6.18 -
6.19 +
6.20 quotient_definition
6.21 "0::int" is "(0::nat, 0::nat)"
6.22
6.23 @@ -292,6 +292,8 @@
6.24 * Theory PReal, including the type "preal" and related operations, has
6.25 been removed. INCOMPATIBILITY.
6.26
6.27 +* Real: new development using Cauchy Sequences.
6.28 +
6.29 * Split off theory "Big_Operators" containing setsum, setprod,
6.30 Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY.
6.31
6.32 @@ -511,6 +513,17 @@
6.33 "sharing_depth", and "show_skolems" options. INCOMPATIBILITY.
6.34 - Removed "nitpick_intro" attribute. INCOMPATIBILITY.
6.35
6.36 +* Method "induct" now takes instantiations of the form t, where t is not
6.37 + a variable, as a shorthand for "x == t", where x is a fresh variable.
6.38 + If this is not intended, t has to be enclosed in parentheses.
6.39 + By default, the equalities generated by definitional instantiations
6.40 + are pre-simplified, which may cause parameters of inductive cases
6.41 + to disappear, or may even delete some of the inductive cases.
6.42 + Use "induct (no_simp)" instead of "induct" to restore the old
6.43 + behaviour. The (no_simp) option is also understood by the "cases"
6.44 + and "nominal_induct" methods, which now perform pre-simplification, too.
6.45 + INCOMPATIBILITY.
6.46 +
6.47
6.48 *** HOLCF ***
6.49
6.50 @@ -683,6 +696,13 @@
6.51 See src/Tools/jEdit or "isabelle jedit" provided by the properly built
6.52 component.
6.53
6.54 +* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono
6.55 +and Bluesky TeX fonts. It provides the usual Isabelle symbols,
6.56 +similar to the default assignment of the document preparation system
6.57 +(cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System
6.58 +provides some operations for direct access to the font without asking
6.59 +the user for manual installation.
6.60 +
6.61
6.62
6.63 New in Isabelle2009-1 (December 2009)
6.64 @@ -3410,8 +3430,6 @@
6.65 * Real: proper support for ML code generation, including 'quickcheck'.
6.66 Reals are implemented as arbitrary precision rationals.
6.67
6.68 -* Real: new development using Cauchy Sequences.
6.69 -
6.70 * Hyperreal: Several constants that previously worked only for the
6.71 reals have been generalized, so they now work over arbitrary vector
6.72 spaces. Type annotations may need to be added in some cases; potential
7.1 --- a/README Mon Jun 21 16:59:37 2010 +0200
7.2 +++ b/README Mon Jun 21 17:41:57 2010 +0200
7.3 @@ -21,10 +21,9 @@
7.4
7.5 Installation
7.6
7.7 - Binary packages are available for Isabelle/HOL etc. for several
7.8 - platforms from the Isabelle web page. The system may be also built
7.9 - from scratch, using the tar.gz source distribution. See file
7.10 - INSTALL as distributed with Isabelle for more information.
7.11 + Completely integrated bundles including the full Isabelle sources,
7.12 + documentation, add-on tools and precompiled logic images for
7.13 + several platforms are available from the Isabelle web page.
7.14
7.15 Further background information may be found in the Isabelle System
7.16 Manual, distributed with the sources (directory doc).
8.1 --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 16:59:37 2010 +0200
8.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 17:41:57 2010 +0200
8.3 @@ -1277,16 +1277,16 @@
8.4 ``strengthened'' inductive statements within the object-logic.
8.5
8.6 \begin{rail}
8.7 - 'cases' (insts * 'and') rule?
8.8 + 'cases' '(no_simp)'? (insts * 'and') rule?
8.9 ;
8.10 - 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
8.11 + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
8.12 ;
8.13 'coinduct' insts taking rule?
8.14 ;
8.15
8.16 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
8.17 ;
8.18 - definst: name ('==' | equiv) term | inst
8.19 + definst: name ('==' | equiv) term | '(' term ')' | inst
8.20 ;
8.21 definsts: ( definst *)
8.22 ;
8.23 @@ -1320,7 +1320,9 @@
8.24 of premises of the case rule; within each premise, the \emph{prefix}
8.25 of variables is instantiated. In most situations, only a single
8.26 term needs to be specified; this refers to the first variable of the
8.27 - last premise (it is usually the same for all cases).
8.28 + last premise (it is usually the same for all cases). The @{text
8.29 + "(no_simp)"} option can be used to disable pre-simplification of
8.30 + cases (see the description of @{method induct} below for details).
8.31
8.32 \item @{method induct}~@{text "insts R"} is analogous to the
8.33 @{method cases} method, but refers to induction rules, which are
8.34 @@ -1342,15 +1344,28 @@
8.35 present in the induction rule. This enables the writer to specify
8.36 only induction variables, or both predicates and variables, for
8.37 example.
8.38 -
8.39 +
8.40 Instantiations may be definitional: equations @{text "x \<equiv> t"}
8.41 introduce local definitions, which are inserted into the claim and
8.42 discharged after applying the induction rule. Equalities reappear
8.43 in the inductive cases, but have been transformed according to the
8.44 induction principle being involved here. In order to achieve
8.45 practically useful induction hypotheses, some variables occurring in
8.46 - @{text t} need to be fixed (see below).
8.47 -
8.48 + @{text t} need to be fixed (see below). Instantiations of the form
8.49 + @{text t}, where @{text t} is not a variable, are taken as a
8.50 + shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
8.51 + variable. If this is not intended, @{text t} has to be enclosed in
8.52 + parentheses. By default, the equalities generated by definitional
8.53 + instantiations are pre-simplified using a specific set of rules,
8.54 + usually consisting of distinctness and injectivity theorems for
8.55 + datatypes. This pre-simplification may cause some of the parameters
8.56 + of an inductive case to disappear, or may even completely delete
8.57 + some of the inductive cases, if one of the equalities occurring in
8.58 + their premises can be simplified to @{text False}. The @{text
8.59 + "(no_simp)"} option can be used to disable pre-simplification.
8.60 + Additional rules to be used in pre-simplification can be declared
8.61 + using the @{attribute_def induct_simp} attribute.
8.62 +
8.63 The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
8.64 specification generalizes variables @{text "x\<^sub>1, \<dots>,
8.65 x\<^sub>m"} of the original goal before applying induction. Thus
9.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 16:59:37 2010 +0200
9.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 17:41:57 2010 +0200
9.3 @@ -1275,16 +1275,16 @@
9.4 ``strengthened'' inductive statements within the object-logic.
9.5
9.6 \begin{rail}
9.7 - 'cases' (insts * 'and') rule?
9.8 + 'cases' '(no_simp)'? (insts * 'and') rule?
9.9 ;
9.10 - 'induct' (definsts * 'and') \\ arbitrary? taking? rule?
9.11 + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule?
9.12 ;
9.13 'coinduct' insts taking rule?
9.14 ;
9.15
9.16 rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
9.17 ;
9.18 - definst: name ('==' | equiv) term | inst
9.19 + definst: name ('==' | equiv) term | '(' term ')' | inst
9.20 ;
9.21 definsts: ( definst *)
9.22 ;
9.23 @@ -1317,7 +1317,8 @@
9.24 of premises of the case rule; within each premise, the \emph{prefix}
9.25 of variables is instantiated. In most situations, only a single
9.26 term needs to be specified; this refers to the first variable of the
9.27 - last premise (it is usually the same for all cases).
9.28 + last premise (it is usually the same for all cases). The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of
9.29 + cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
9.30
9.31 \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the
9.32 \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
9.33 @@ -1339,15 +1340,27 @@
9.34 present in the induction rule. This enables the writer to specify
9.35 only induction variables, or both predicates and variables, for
9.36 example.
9.37 -
9.38 +
9.39 Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}
9.40 introduce local definitions, which are inserted into the claim and
9.41 discharged after applying the induction rule. Equalities reappear
9.42 in the inductive cases, but have been transformed according to the
9.43 induction principle being involved here. In order to achieve
9.44 practically useful induction hypotheses, some variables occurring in
9.45 - \isa{t} need to be fixed (see below).
9.46 -
9.47 + \isa{t} need to be fixed (see below). Instantiations of the form
9.48 + \isa{t}, where \isa{t} is not a variable, are taken as a
9.49 + shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh
9.50 + variable. If this is not intended, \isa{t} has to be enclosed in
9.51 + parentheses. By default, the equalities generated by definitional
9.52 + instantiations are pre-simplified using a specific set of rules,
9.53 + usually consisting of distinctness and injectivity theorems for
9.54 + datatypes. This pre-simplification may cause some of the parameters
9.55 + of an inductive case to disappear, or may even completely delete
9.56 + some of the inductive cases, if one of the equalities occurring in
9.57 + their premises can be simplified to \isa{False}. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification.
9.58 + Additional rules to be used in pre-simplification can be declared
9.59 + using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute.
9.60 +
9.61 The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}''
9.62 specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus
9.63 induction hypotheses may become sufficiently general to get the
10.1 --- a/doc-src/Ref/introduction.tex Mon Jun 21 16:59:37 2010 +0200
10.2 +++ b/doc-src/Ref/introduction.tex Mon Jun 21 17:41:57 2010 +0200
10.3 @@ -5,9 +5,7 @@
10.4 \index{starting up|bold}\nobreak
10.5 %
10.6 We assume that your local Isabelle administrator (this might be you!) has
10.7 -already installed the Isabelle system together with appropriate object-logics
10.8 ---- otherwise see the \texttt{README} and \texttt{INSTALL} files in the
10.9 -top-level directory of the distribution on how to do this.
10.10 +already installed the Isabelle system together with appropriate object-logics.
10.11
10.12 \medskip Let $\langle isabellehome \rangle$ denote the location where
10.13 the distribution has been installed. To run Isabelle from a the shell
11.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 16:59:37 2010 +0200
11.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 17:41:57 2010 +0200
11.3 @@ -491,11 +491,11 @@
11.4 and b: "\<Gamma> \<turnstile> e' : T'"
11.5 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
11.6 using a b
11.7 -proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
11.8 +proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
11.9 case (t_VAR y T x e' \<Delta>)
11.10 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
11.11 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
11.12 - and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
11.13 + and a3: "\<Gamma> \<turnstile> e' : T'" .
11.14 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
11.15 { assume eq: "x=y"
11.16 from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
12.1 --- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 16:59:37 2010 +0200
12.2 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 17:41:57 2010 +0200
12.3 @@ -141,11 +141,11 @@
12.4 and b: "\<Gamma> \<turnstile> e' : T'"
12.5 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T"
12.6 using a b
12.7 -proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
12.8 +proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
12.9 case (t_Var y T x e' \<Delta>)
12.10 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)"
12.11 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)"
12.12 - and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all
12.13 + and a3: "\<Gamma> \<turnstile> e' : T'" .
12.14 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert)
12.15 { assume eq: "x=y"
12.16 from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
13.1 --- a/src/HOL/Nominal/INSTALL Mon Jun 21 16:59:37 2010 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,57 +0,0 @@
13.4 -
13.5 -Installation Notes for the Nominal Datatype Package
13.6 -===================================================
13.7 -
13.8 -Although the nominal datatype package is an official
13.9 -package in the development snapshot of Isabelle, we
13.10 -keep a semi-official snapshot of Isabelle and Nominal
13.11 -under
13.12 -
13.13 - http://isabelle.in.tum.de/nominal/
13.14 -
13.15 -This snapshot contains the latest stable release of the
13.16 -nominal datatype package.
13.17 -
13.18 -To install it, follow the instructions of Isabelle's INSTALL
13.19 -about how a snap-shot can be set up. The building process
13.20 -needs to be started inside the [ISABELLE_HOME] directory with
13.21 -the command:
13.22 -
13.23 - ./build -m HOL-Nominal
13.24 -
13.25 -After the build completes, install the files with the command
13.26 -
13.27 - ./bin/isabelle install -p /usr/local/bin
13.28 -
13.29 -where /usr/local/bin needs to be replaced by an appropriate
13.30 -directory, if you are not root on the system.
13.31 -
13.32 -The sources of the nominal datatype package can be found
13.33 -in the directory
13.34 -
13.35 - [ISABELLE_HOME]/src/HOL/Nominal
13.36 -
13.37 -The examples are in
13.38 -
13.39 - [ISABELLE_HOME]/src/HOL/Nominal/Examples
13.40 -
13.41 -Starting Isabelle with the Nominal Datatype Package Preloaded
13.42 -=============================================================
13.43 -
13.44 -Isabelle and the Proof-General interface can be started
13.45 -with
13.46 -
13.47 - Isabelle -L HOL-Nominal <<theory file to be opened>> &
13.48 -
13.49 -on the command-line. This automatically loads the correct
13.50 -keyword file needed for the nominal datatype package.
13.51 -
13.52 -Problems with starting Isabelle and Proof-General usually
13.53 -come from old versions of Proof-General. So make sure you
13.54 -have installed at least the version ProofGeneral-3.6pre050930.
13.55 -
13.56 -If you have problems or comments about the installation process,
13.57 -please make use of the nominal mailing list at
13.58 -
13.59 -https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/
13.60 -
14.1 --- a/src/Pure/General/pretty.scala Mon Jun 21 16:59:37 2010 +0200
14.2 +++ b/src/Pure/General/pretty.scala Mon Jun 21 17:41:57 2010 +0200
14.3 @@ -134,7 +134,7 @@
14.4
14.5 def string_of(input: List[XML.Tree], margin: Int = margin_default,
14.6 metric: String => Double = metric_default): String =
14.7 - formatted(input).iterator.flatMap(XML.content).mkString
14.8 + formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
14.9
14.10
14.11 /* unformatted output */
15.1 --- a/src/Pure/Isar/runtime.ML Mon Jun 21 16:59:37 2010 +0200
15.2 +++ b/src/Pure/Isar/runtime.ML Mon Jun 21 17:41:57 2010 +0200
15.3 @@ -54,6 +54,7 @@
15.4 val detailed = ! Output.debugging;
15.5
15.6 fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
15.7 + | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
15.8 | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
15.9 | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
15.10 exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
16.1 --- a/src/Pure/PIDE/command.scala Mon Jun 21 16:59:37 2010 +0200
16.2 +++ b/src/Pure/PIDE/command.scala Mon Jun 21 17:41:57 2010 +0200
16.3 @@ -48,8 +48,7 @@
16.4
16.5 def name: String = if (is_command) span.head.content else ""
16.6 override def toString =
16.7 - if (is_command) name + "(" + id + ")"
16.8 - else if (is_ignored) "<ignored>" else "<malformed>"
16.9 + id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
16.10
16.11
16.12 /* source text */
17.1 --- a/src/Pure/System/isabelle_system.scala Mon Jun 21 16:59:37 2010 +0200
17.2 +++ b/src/Pure/System/isabelle_system.scala Mon Jun 21 17:41:57 2010 +0200
17.3 @@ -12,6 +12,7 @@
17.4 BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
17.5 File, IOException}
17.6 import java.awt.{GraphicsEnvironment, Font}
17.7 +import java.awt.font.TextAttribute
17.8
17.9 import scala.io.Source
17.10 import scala.util.matching.Regex
17.11 @@ -336,31 +337,23 @@
17.12 /* fonts */
17.13
17.14 val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
17.15 + val font_family_default = "IsabelleText"
17.16
17.17 def get_font(size: Int = 1, bold: Boolean = false): Font =
17.18 new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
17.19
17.20 + def create_default_font(bold: Boolean = false): Font =
17.21 + if (bold)
17.22 + Font.createFont(Font.TRUETYPE_FONT,
17.23 + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
17.24 + else
17.25 + Font.createFont(Font.TRUETYPE_FONT,
17.26 + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
17.27 +
17.28 def install_fonts()
17.29 {
17.30 - def create_font(bold: Boolean): Font =
17.31 - {
17.32 - val name =
17.33 - if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
17.34 - else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
17.35 - Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
17.36 - }
17.37 - def check_font() = get_font().getFamily == font_family
17.38 -
17.39 - if (!check_font()) {
17.40 - val font = create_font(false)
17.41 - val bold_font = create_font(true)
17.42 -
17.43 - val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
17.44 - ge.registerFont(font)
17.45 - // workaround strange problem with Apple's Java 1.6 font manager
17.46 - // FIXME does not quite work!?
17.47 - if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
17.48 - if (!check_font()) error("Failed to install IsabelleText fonts")
17.49 - }
17.50 + val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
17.51 + ge.registerFont(create_default_font(bold = false))
17.52 + ge.registerFont(create_default_font(bold = true))
17.53 }
17.54 }
18.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 16:59:37 2010 +0200
18.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 17:41:57 2010 +0200
18.3 @@ -155,9 +155,11 @@
18.4 def to: Int => Int = model.to_current(document, _)
18.5 def from: Int => Int = model.from_current(document, _)
18.6
18.7 + /* FIXME
18.8 for (text_area <- Isabelle.jedit_text_areas(model.buffer)
18.9 if Document_View(text_area).isDefined)
18.10 Document_View(text_area).get.set_styles()
18.11 + */
18.12
18.13 def handle_token(style: Byte, offset: Int, length: Int) =
18.14 handler.handleToken(line_segment, style, offset, length, context)
19.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 16:59:37 2010 +0200
19.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 17:41:57 2010 +0200
19.3 @@ -129,19 +129,18 @@
19.4 reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
19.5 }
19.6 tracing.selected = show_tracing
19.7 - tracing.tooltip =
19.8 - "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
19.9 + tracing.tooltip = "Indicate output of tracing messages"
19.10
19.11 private val auto_update = new CheckBox("Auto update") {
19.12 reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
19.13 }
19.14 auto_update.selected = follow_caret
19.15 - auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
19.16 + auto_update.tooltip = "Indicate automatic update following cursor movement"
19.17
19.18 private val update = new Button("Update") {
19.19 reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
19.20 }
19.21 - update.tooltip = "<html>Update display according to the command at cursor position</html>"
19.22 + update.tooltip = "Update display according to the command at cursor position"
19.23
19.24 val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
19.25 add(controls.peer, BorderLayout.NORTH)