NEWS
author haftmann
Fri Mar 16 21:32:06 2007 +0100 (2007-03-16)
changeset 22450 51ee032f9591
parent 22422 ee19cdb07528
child 22735 cf627add250a
permissions -rw-r--r--
lattice cleanup
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     3 
     4 New in this Isabelle version
     5 ----------------------------
     6 
     7 *** General ***
     8 
     9 * Theory syntax: the header format ``theory A = B + C:'' has been
    10 discontinued in favour of ``theory A imports B C begin''.  Use isatool
    11 fixheaders to convert existing theory files.  INCOMPATIBILITY.
    12 
    13 * Theory syntax: the old non-Isar theory file format has been
    14 discontinued altogether.  Note that ML proof scripts may still be used
    15 with Isar theories; migration is usually quite simple with the ML
    16 function use_legacy_bindings.  INCOMPATIBILITY.
    17 
    18 * Theory syntax: some popular names (e.g. "class", "fun", "help",
    19 "if") are now keywords.  INCOMPATIBILITY, use double quotes.
    20 
    21 * Legacy goal package: reduced interface to the bare minimum required
    22 to keep existing proof scripts running.  Most other user-level
    23 functions are now part of the OldGoals structure, which is *not* open
    24 by default (consider isatool expandshort before open OldGoals).
    25 Removed top_sg, prin, printyp, pprint_term/typ altogether, because
    26 these tend to cause confusion about the actual goal (!) context being
    27 used here, which is not necessarily the same as the_context().
    28 
    29 * Command 'find_theorems': support "*" wildcard in "name:" criterion.
    30 
    31 * The ``prems limit'' option (cf. ProofContext.prems_limit) is now -1
    32 by default, which means that "prems" (and also "fixed variables") are
    33 suppressed from proof state output.  Note that the ProofGeneral
    34 settings mechanism allows to change and save options persistently, but
    35 older versions of Isabelle will fail to start up if a negative prems
    36 limit is imposed.
    37 
    38 * Local theory targets may be specified by non-nested blocks of
    39 ``context/locale/class ... begin'' followed by ``end''.  The body may
    40 contain definitions, theorems etc., including any derived mechanism
    41 that has been implemented on top of these primitives.  This concept
    42 generalizes the existing ``theorem (in ...)'' towards more versatility
    43 and scalability.
    44 
    45 * Proof General interface: proper undo of final 'end' command;
    46 discontinued Isabelle/classic mode (ML proof scripts).
    47 
    48 
    49 *** Document preparation ***
    50 
    51 * Added antiquotation @{theory name} which prints the given name,
    52 after checking that it refers to a valid ancestor theory in the
    53 current context.
    54 
    55 * Added antiquotations @{ML_type text} and @{ML_struct text} which
    56 check the given source text as ML type/structure, printing verbatim.
    57 
    58 * Added antiquotation @{abbrev "c args"} which prints the abbreviation
    59 "c args == rhs" given in the current context.  (Any number of
    60 arguments may be given on the LHS.)
    61 
    62 
    63 
    64 *** Pure ***
    65 
    66 * class_package.ML offers a combination of axclasses and locales to
    67 achieve Haskell-like type classes in Isabelle. See
    68 HOL/ex/Classpackage.thy for examples.
    69 
    70 * Yet another code generator framework allows to generate executable
    71 code for ML and Haskell (including "class"es). A short usage sketch:
    72 
    73     internal compilation:
    74         code_gen <list of constants (term syntax)> (SML #)
    75     writing SML code to a file:
    76         code_gen <list of constants (term syntax)> (SML <filename>)
    77     writing Haskell code to a bunch of files:
    78         code_gen <list of constants (term syntax)> (Haskell <filename>)
    79 
    80 Reasonable default setup of framework in HOL/Main.
    81 
    82 Theorem attributs for selecting and transforming function equations theorems:
    83 
    84     [code fun]:       select a theorem as function equation for a specific constant
    85     [code nofun]:     deselect a theorem as function equation for a specific constant
    86     [code inline]:    select an equation theorem for unfolding (inlining) in place
    87     [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
    88 
    89 User-defined serializations (target in {SML, Haskell}):
    90 
    91     code_const <and-list of constants (term syntax)>
    92       {(target) <and-list of const target syntax>}+
    93 
    94     code_type <and-list of type constructors>
    95       {(target) <and-list of type target syntax>}+
    96 
    97     code_instance <and-list of instances>
    98       {(target)}+
    99         where instance ::= <type constructor> :: <class>
   100 
   101     code_class <and_list of classes>
   102       {(target) <and-list of class target syntax>}+
   103         where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
   104 
   105 For code_instance and code_class, target SML is silently ignored.
   106 
   107 See HOL theories and HOL/ex/Code*.thy for usage examples.  Doc/Isar/Advanced/Codegen/
   108 provides a tutorial.
   109 
   110 * Command 'no_translations' removes translation rules from theory
   111 syntax.
   112 
   113 * Overloaded definitions are now actually checked for acyclic
   114 dependencies.  The overloading scheme is slightly more general than
   115 that of Haskell98, although Isabelle does not demand an exact
   116 correspondence to type class and instance declarations.
   117 INCOMPATIBILITY, use ``defs (unchecked overloaded)'' to admit more
   118 exotic versions of overloading -- at the discretion of the user!
   119 
   120 Polymorphic constants are represented via type arguments, i.e. the
   121 instantiation that matches an instance against the most general
   122 declaration given in the signature.  For example, with the declaration
   123 c :: 'a => 'a => 'a, an instance c :: nat => nat => nat is represented
   124 as c(nat).  Overloading is essentially simultaneous structural
   125 recursion over such type arguments.  Incomplete specification patterns
   126 impose global constraints on all occurrences, e.g. c('a * 'a) on the
   127 LHS means that more general c('a * 'b) will be disallowed on any RHS.
   128 Command 'print_theory' outputs the normalized system of recursive
   129 equations, see section "definitions".
   130 
   131 * Isar: improper proof element 'guess' is like 'obtain', but derives
   132 the obtained context from the course of reasoning!  For example:
   133 
   134   assume "EX x y. A x & B y"   -- "any previous fact"
   135   then guess x and y by clarify
   136 
   137 This technique is potentially adventurous, depending on the facts and
   138 proof tools being involved here.
   139 
   140 * Isar: known facts from the proof context may be specified as literal
   141 propositions, using ASCII back-quote syntax.  This works wherever
   142 named facts used to be allowed so far, in proof commands, proof
   143 methods, attributes etc.  Literal facts are retrieved from the context
   144 according to unification of type and term parameters.  For example,
   145 provided that "A" and "A ==> B" and "!!x. P x ==> Q x" are known
   146 theorems in the current context, then these are valid literal facts:
   147 `A` and `A ==> B` and `!!x. P x ==> Q x" as well as `P a ==> Q a` etc.
   148 
   149 There is also a proof method "fact" which does the same composition
   150 for explicit goal states, e.g. the following proof texts coincide with
   151 certain special cases of literal facts:
   152 
   153   have "A" by fact                 ==  note `A`
   154   have "A ==> B" by fact           ==  note `A ==> B`
   155   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
   156   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
   157 
   158 * Isar: ":" (colon) is no longer a symbolic identifier character in
   159 outer syntax.  Thus symbolic identifiers may be used without
   160 additional white space in declarations like this: ``assume *: A''.
   161 
   162 * Isar: 'print_facts' prints all local facts of the current context,
   163 both named and unnamed ones.
   164 
   165 * Isar: 'def' now admits simultaneous definitions, e.g.:
   166 
   167   def x == "t" and y == "u"
   168 
   169 * Isar: added command 'unfolding', which is structurally similar to
   170 'using', but affects both the goal state and facts by unfolding given
   171 rewrite rules.  Thus many occurrences of the 'unfold' method or
   172 'unfolded' attribute may be replaced by first-class proof text.
   173 
   174 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded',
   175 and command 'unfolding' now all support object-level equalities
   176 (potentially conditional).  The underlying notion of rewrite rule is
   177 analogous to the 'rule_format' attribute, but *not* that of the
   178 Simplifier (which is usually more generous).
   179 
   180 * Isar: the goal restriction operator [N] (default N = 1) evaluates a
   181 method expression within a sandbox consisting of the first N
   182 sub-goals, which need to exist.  For example, ``simp_all [3]''
   183 simplifies the first three sub-goals, while (rule foo, simp_all)[]
   184 simplifies all new goals that emerge from applying rule foo to the
   185 originally first one.
   186 
   187 * Isar: schematic goals are no longer restricted to higher-order
   188 patterns; e.g. ``lemma "?P(?x)" by (rule TrueI)'' now works as
   189 expected.
   190 
   191 * Isar: the conclusion of a long theorem statement is now either
   192 'shows' (a simultaneous conjunction, as before), or 'obtains'
   193 (essentially a disjunction of cases with local parameters and
   194 assumptions).  The latter allows to express general elimination rules
   195 adequately; in this notation common elimination rules look like this:
   196 
   197   lemma exE:    -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis"
   198     assumes "EX x. P x"
   199     obtains x where "P x"
   200 
   201   lemma conjE:  -- "A & B ==> (A ==> B ==> thesis) ==> thesis"
   202     assumes "A & B"
   203     obtains A and B
   204 
   205   lemma disjE:  -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis"
   206     assumes "A | B"
   207     obtains
   208       A
   209     | B
   210 
   211 The subsequent classical rules even refer to the formal "thesis"
   212 explicitly:
   213 
   214   lemma classical:     -- "(~ thesis ==> thesis) ==> thesis"
   215     obtains "~ thesis"
   216 
   217   lemma Peirce's_Law:  -- "((thesis ==> something) ==> thesis) ==> thesis"
   218     obtains "thesis ==> something"
   219 
   220 The actual proof of an 'obtains' statement is analogous to that of the
   221 Isar proof element 'obtain', only that there may be several cases.
   222 Optional case names may be specified in parentheses; these will be
   223 available both in the present proof and as annotations in the
   224 resulting rule, for later use with the 'cases' method (cf. attribute
   225 case_names).
   226 
   227 * Isar: the assumptions of a long theorem statement are available as
   228 "assms" fact in the proof context.  This is more appropriate than the
   229 (historical) "prems", which refers to all assumptions of the current
   230 context, including those from the target locale, proof body etc.
   231 
   232 * Isar: 'print_statement' prints theorems from the current theory or
   233 proof context in long statement form, according to the syntax of a
   234 top-level lemma.
   235 
   236 * Isar: 'obtain' takes an optional case name for the local context
   237 introduction rule (default "that").
   238 
   239 * Isar: removed obsolete 'concl is' patterns.  INCOMPATIBILITY, use
   240 explicit (is "_ ==> ?foo") in the rare cases where this still happens
   241 to occur.
   242 
   243 * Pure: syntax "CONST name" produces a fully internalized constant
   244 according to the current context.  This is particularly useful for
   245 syntax translations that should refer to internal constant
   246 representations independently of name spaces.
   247 
   248 * Pure: syntax constant for foo (binder "FOO ") is called "foo_binder"
   249 instead of "FOO ". This allows multiple binder declarations to coexist
   250 in the same context.  INCOMPATIBILITY.
   251 
   252 * Isar/locales: 'notation' provides a robust interface to the 'syntax'
   253 primitive that also works in a locale context (both for constants and
   254 fixed variables).  Type declaration and internal syntactic
   255 representation of given constants retrieved from the context.
   256 
   257 * Isar/locales: new derived specification elements 'axiomatization',
   258 'definition', 'abbreviation', which support type-inference, admit
   259 object-level specifications (equality, equivalence).  See also the
   260 isar-ref manual.  Examples:
   261 
   262   axiomatization
   263     eq  (infix "===" 50) where
   264     eq_refl: "x === x" and eq_subst: "x === y ==> P x ==> P y"
   265 
   266   definition "f x y = x + y + 1"
   267   definition g where "g x = f x x"
   268 
   269   abbreviation
   270     neq  (infix "=!=" 50) where
   271     "x =!= y == ~ (x === y)"
   272 
   273 These specifications may be also used in a locale context.  Then the
   274 constants being introduced depend on certain fixed parameters, and the
   275 constant name is qualified by the locale base name.  An internal
   276 abbreviation takes care for convenient input and output, making the
   277 parameters implicit and using the original short name.  See also
   278 HOL/ex/Abstract_NAT.thy for an example of deriving polymorphic
   279 entities from a monomorphic theory.
   280 
   281 Presently, abbreviations are only available 'in' a target locale, but
   282 not inherited by general import expressions.  Also note that
   283 'abbreviation' may be used as a type-safe replacement for 'syntax' +
   284 'translations' in common applications.
   285 
   286 Concrete syntax is attached to specified constants in internal form,
   287 independently of name spaces.  The parse tree representation is
   288 slightly different -- use 'notation' instead of raw 'syntax', and
   289 'translations' with explicit "CONST" markup to accommodate this.
   290 
   291 * Pure: command 'print_abbrevs' prints all constant abbreviations of
   292 the current context.  Print mode "no_abbrevs" prevents inversion of
   293 abbreviations on output.
   294 
   295 * Isar/locales: improved parameter handling:
   296 - use of locales "var" and "struct" no longer necessary;
   297 - parameter renamings are no longer required to be injective.
   298   This enables, for example, to define a locale for endomorphisms thus:
   299   locale endom = homom mult mult h.
   300 
   301 * Isar/locales: changed the way locales with predicates are defined.
   302 Instead of accumulating the specification, the imported expression is
   303 now an interpretation.  INCOMPATIBILITY: different normal form of
   304 locale expressions.  In particular, in interpretations of locales with
   305 predicates, goals repesenting already interpreted fragments are not
   306 removed automatically.  Use methods `intro_locales' and
   307 `unfold_locales'; see below.
   308 
   309 * Isar/locales: new methods `intro_locales' and `unfold_locales'
   310 provide backward reasoning on locales predicates.  The methods are
   311 aware of interpretations and discharge corresponding goals.
   312 `intro_locales' is less aggressive then `unfold_locales' and does not
   313 unfold predicates to assumptions.
   314 
   315 * Isar/locales: the order in which locale fragments are accumulated
   316 has changed.  This enables to override declarations from fragments due
   317 to interpretations -- for example, unwanted simp rules.
   318 
   319 * Provers/induct: improved internal context management to support
   320 local fixes and defines on-the-fly.  Thus explicit meta-level
   321 connectives !! and ==> are rarely required anymore in inductive goals
   322 (using object-logic connectives for this purpose has been long
   323 obsolete anyway).  The subsequent proof patterns illustrate advanced
   324 techniques of natural induction; general datatypes and inductive sets
   325 work analogously (see also src/HOL/Lambda for realistic examples).
   326 
   327 (1) This is how to ``strengthen'' an inductive goal wrt. certain
   328 parameters:
   329 
   330   lemma
   331     fixes n :: nat and x :: 'a
   332     assumes a: "A n x"
   333     shows "P n x"
   334     using a                     -- {* make induct insert fact a *}
   335   proof (induct n arbitrary: x) -- {* generalize goal to "!!x. A n x ==> P n x" *}
   336     case 0
   337     show ?case sorry
   338   next
   339     case (Suc n)
   340     note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
   341     note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
   342     show ?case sorry
   343   qed
   344 
   345 (2) This is how to perform induction over ``expressions of a certain
   346 form'', using a locally defined inductive parameter n == "a x"
   347 together with strengthening (the latter is usually required to get
   348 sufficiently flexible induction hypotheses):
   349 
   350   lemma
   351     fixes a :: "'a => nat"
   352     assumes a: "A (a x)"
   353     shows "P (a x)"
   354     using a
   355   proof (induct n == "a x" arbitrary: x)
   356     ...
   357 
   358 See also HOL/Isar_examples/Puzzle.thy for an application of the this
   359 particular technique.
   360 
   361 (3) This is how to perform existential reasoning ('obtains' or
   362 'obtain') by induction, while avoiding explicit object-logic
   363 encodings:
   364 
   365   lemma
   366     fixes n :: nat
   367     obtains x :: 'a where "P n x" and "Q n x"
   368   proof (induct n arbitrary: thesis)
   369     case 0
   370     obtain x where "P 0 x" and "Q 0 x" sorry
   371     then show thesis by (rule 0)
   372   next
   373     case (Suc n)
   374     obtain x where "P n x" and "Q n x" by (rule Suc.hyps)
   375     obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry
   376     then show thesis by (rule Suc.prems)
   377   qed
   378 
   379 Here the 'arbitrary: thesis' specification essentially modifies the
   380 scope of the formal thesis parameter, in order to the get the whole
   381 existence statement through the induction as expected.
   382 
   383 * Provers/induct: mutual induction rules are now specified as a list
   384 of rule sharing the same induction cases.  HOL packages usually
   385 provide foo_bar.inducts for mutually defined items foo and bar
   386 (e.g. inductive sets or datatypes).  INCOMPATIBILITY, users need to
   387 specify mutual induction rules differently, i.e. like this:
   388 
   389   (induct rule: foo_bar.inducts)
   390   (induct set: foo bar)
   391   (induct type: foo bar)
   392 
   393 The ML function ProjectRule.projections turns old-style rules into the
   394 new format.
   395 
   396 * Provers/induct: improved handling of simultaneous goals.  Instead of
   397 introducing object-level conjunction, the statement is now split into
   398 several conclusions, while the corresponding symbolic cases are
   399 nested accordingly.  INCOMPATIBILITY, proofs need to be structured
   400 explicitly.  For example:
   401 
   402   lemma
   403     fixes n :: nat
   404     shows "P n" and "Q n"
   405   proof (induct n)
   406     case 0 case 1
   407     show "P 0" sorry
   408   next
   409     case 0 case 2
   410     show "Q 0" sorry
   411   next
   412     case (Suc n) case 1
   413     note `P n` and `Q n`
   414     show "P (Suc n)" sorry
   415   next
   416     case (Suc n) case 2
   417     note `P n` and `Q n`
   418     show "Q (Suc n)" sorry
   419   qed
   420 
   421 The split into subcases may be deferred as follows -- this is
   422 particularly relevant for goal statements with local premises.
   423 
   424   lemma
   425     fixes n :: nat
   426     shows "A n ==> P n" and "B n ==> Q n"
   427   proof (induct n)
   428     case 0
   429     {
   430       case 1
   431       note `A 0`
   432       show "P 0" sorry
   433     next
   434       case 2
   435       note `B 0`
   436       show "Q 0" sorry
   437     }
   438   next
   439     case (Suc n)
   440     note `A n ==> P n` and `B n ==> Q n`
   441     {
   442       case 1
   443       note `A (Suc n)`
   444       show "P (Suc n)" sorry
   445     next
   446       case 2
   447       note `B (Suc n)`
   448       show "Q (Suc n)" sorry
   449     }
   450   qed
   451 
   452 If simultaneous goals are to be used with mutual rules, the statement
   453 needs to be structured carefully as a two-level conjunction, using
   454 lists of propositions separated by 'and':
   455 
   456   lemma
   457     shows "a : A ==> P1 a"
   458           "a : A ==> P2 a"
   459       and "b : B ==> Q1 b"
   460           "b : B ==> Q2 b"
   461           "b : B ==> Q3 b"
   462   proof (induct set: A B)
   463 
   464 * Provers/induct: support coinduction as well.  See
   465 src/HOL/Library/Coinductive_List.thy for various examples.
   466 
   467 * Attribute "symmetric" produces result with standardized schematic
   468 variables (index 0).  Potential INCOMPATIBILITY.
   469 
   470 * Simplifier: by default the simplifier trace only shows top level
   471 rewrites now. That is, trace_simp_depth_limit is set to 1 by
   472 default. Thus there is less danger of being flooded by the trace. The
   473 trace indicates where parts have been suppressed.
   474   
   475 * Provers/classical: removed obsolete classical version of elim_format
   476 attribute; classical elim/dest rules are now treated uniformly when
   477 manipulating the claset.
   478 
   479 * Provers/classical: stricter checks to ensure that supplied intro,
   480 dest and elim rules are well-formed; dest and elim rules must have at
   481 least one premise.
   482 
   483 * Provers/classical: attributes dest/elim/intro take an optional
   484 weight argument for the rule (just as the Pure versions).  Weights are
   485 ignored by automated tools, but determine the search order of single
   486 rule steps.
   487 
   488 * Syntax: input syntax now supports dummy variable binding "%_. b",
   489 where the body does not mention the bound variable.  Note that dummy
   490 patterns implicitly depend on their context of bounds, which makes
   491 "{_. _}" match any set comprehension as expected.  Potential
   492 INCOMPATIBILITY -- parse translations need to cope with syntactic
   493 constant "_idtdummy" in the binding position.
   494 
   495 * Syntax: removed obsolete syntactic constant "_K" and its associated
   496 parse translation.  INCOMPATIBILITY -- use dummy abstraction instead,
   497 for example "A -> B" => "Pi A (%_. B)".
   498 
   499 * Pure: 'class_deps' command visualizes the subclass relation, using
   500 the graph browser tool.
   501 
   502 * Pure: 'print_theory' now suppresses entities with internal name
   503 (trailing "_") by default; use '!' option for full details.
   504 
   505 
   506 *** HOL ***
   507 
   508 * Some steps towards more uniform lattice theory development in HOL.
   509 
   510     constants "meet" and "join" now named "inf" and "sup"
   511     constant "Meet" now named "Inf"
   512 
   513     classes "meet_semilorder" and "join_semilorder" now named
   514       "lower_semilattice" and "upper_semilattice"
   515     class "lorder" now named "lattice"
   516     class "comp_lat" now named "complete_lattice"
   517 
   518     Instantiation of lattice classes allows explicit definitions
   519     for "inf" and "sup" operations.
   520 
   521   INCOMPATIBILITY. Theorem renames:
   522 
   523     meet_left_le            ~> inf_le1
   524     meet_right_le           ~> inf_le2
   525     join_left_le            ~> sup_ge1
   526     join_right_le           ~> sup_ge2
   527     meet_join_le            ~> inf_sup_ord
   528     le_meetI                ~> le_infI
   529     join_leI                ~> le_supI
   530     le_meet                 ~> le_inf_iff
   531     le_join                 ~> ge_sup_conv
   532     meet_idempotent         ~> inf_idem
   533     join_idempotent         ~> sup_idem
   534     meet_comm               ~> inf_commute
   535     join_comm               ~> sup_commute
   536     meet_leI1               ~> le_infI1
   537     meet_leI2               ~> le_infI2
   538     le_joinI1               ~> le_supI1
   539     le_joinI2               ~> le_supI2
   540     meet_assoc              ~> inf_assoc
   541     join_assoc              ~> sup_assoc
   542     meet_left_comm          ~> inf_left_commute
   543     meet_left_idempotent    ~> inf_left_idem
   544     join_left_comm          ~> sup_left_commute
   545     join_left_idempotent    ~> sup_left_idem
   546     meet_aci                ~> inf_aci
   547     join_aci                ~> sup_aci
   548     le_def_meet             ~> le_iff_inf
   549     le_def_join             ~> le_iff_sup
   550     join_absorp2            ~> sup_absorb2
   551     join_absorp1            ~> sup_absorb1
   552     meet_absorp1            ~> inf_absorb1
   553     meet_absorp2            ~> inf_absorb2
   554     meet_join_absorp        ~> inf_sup_absorb
   555     join_meet_absorp        ~> sup_inf_absorb
   556     distrib_join_le         ~> distrib_sup_le
   557     distrib_meet_le         ~> distrib_inf_le
   558 
   559     add_meet_distrib_left   ~> add_inf_distrib_left
   560     add_join_distrib_left   ~> add_sup_distrib_left
   561     is_join_neg_meet        ~> is_join_neg_inf
   562     is_meet_neg_join        ~> is_meet_neg_sup
   563     add_meet_distrib_right  ~> add_inf_distrib_right
   564     add_join_distrib_right  ~> add_sup_distrib_right
   565     add_meet_join_distribs  ~> add_sup_inf_distribs
   566     join_eq_neg_meet        ~> sup_eq_neg_inf
   567     meet_eq_neg_join        ~> inf_eq_neg_sup
   568     add_eq_meet_join        ~> add_eq_inf_sup
   569     meet_0_imp_0            ~> inf_0_imp_0
   570     join_0_imp_0            ~> sup_0_imp_0
   571     meet_0_eq_0             ~> inf_0_eq_0
   572     join_0_eq_0             ~> sup_0_eq_0
   573     neg_meet_eq_join        ~> neg_inf_eq_sup
   574     neg_join_eq_meet        ~> neg_sup_eq_inf
   575     join_eq_if              ~> sup_eq_if
   576 
   577     mono_meet               ~> mono_inf
   578     mono_join               ~> mono_sup
   579     meet_bool_eq            ~> inf_bool_eq
   580     join_bool_eq            ~> sup_bool_eq
   581     meet_fun_eq             ~> inf_fun_eq
   582     join_fun_eq             ~> sup_fun_eq
   583     meet_set_eq             ~> inf_set_eq
   584     join_set_eq             ~> sup_set_eq
   585     meet1_iff               ~> inf1_iff
   586     meet2_iff               ~> inf2_iff
   587     meet1I                  ~> inf1I
   588     meet2I                  ~> inf2I
   589     meet1D1                 ~> inf1D1
   590     meet2D1                 ~> inf2D1
   591     meet1D2                 ~> inf1D2
   592     meet2D2                 ~> inf2D2
   593     meet1E                  ~> inf1E
   594     meet2E                  ~> inf2E
   595     join1_iff               ~> sup1_iff
   596     join2_iff               ~> sup2_iff
   597     join1I1                 ~> sup1I1
   598     join2I1                 ~> sup2I1
   599     join1I1                 ~> sup1I1
   600     join2I2                 ~> sup1I2
   601     join1CI                 ~> sup1CI
   602     join2CI                 ~> sup2CI
   603     join1E                  ~> sup1E
   604     join2E                  ~> sup2E
   605 
   606     is_meet_Meet            ~> is_meet_Inf
   607     Meet_bool_def           ~> Inf_bool_def
   608     Meet_fun_def            ~> Inf_fun_def
   609     Meet_greatest           ~> Inf_greatest
   610     Meet_lower              ~> Inf_lower
   611     Meet_set_def            ~> Inf_set_def
   612 
   613     listsp_meetI            ~> listsp_infI
   614     listsp_meet_eq          ~> listsp_inf_eq
   615 
   616     meet_min                ~> inf_min
   617     join_max                ~> sup_max
   618 
   619 * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
   620 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
   621 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
   622 
   623 * Addes class (axclass + locale) "preorder" as superclass of "order";
   624 potential INCOMPATIBILITY: order of proof goals in order/linorder instance
   625 proofs changed.
   626 
   627 * Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
   628 INCOMPATIBILITY.
   629 
   630 * Dropped lemma duplicate if_def2 in favor of if_bool_eq_conj.
   631 INCOMPATIBILITY.
   632 
   633 * Added syntactic class "size"; overloaded constant "size" now has
   634 type "'a::size ==> bool"
   635 
   636 * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
   637 dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
   638 
   639 * Added method "lexicographic_order" automatically synthesizes
   640 termination relations as lexicographic combinations of size measures
   641 -- 'function' package.
   642 
   643 * HOL/records: generalised field-update to take a function on the
   644 field rather than the new value: r(|A := x|) is translated to A_update
   645 (K x) r The K-combinator that is internally used is called K_record.
   646 INCOMPATIBILITY: Usage of the plain update functions has to be
   647 adapted.
   648  
   649 * axclass "semiring_0" now contains annihilation axioms x * 0 = 0 and
   650 0 * x = 0, which are required for a semiring.  Richer structures do
   651 not inherit from semiring_0 anymore, because this property is a
   652 theorem there, not an axiom.  INCOMPATIBILITY: In instances of
   653 semiring_0, there is more to prove, but this is mostly trivial.
   654 
   655 * axclass "recpower" was generalized to arbitrary monoids, not just
   656 commutative semirings.  INCOMPATIBILITY: If you use recpower and need
   657 commutativity or a semiring property, add the corresponding classes.
   658 
   659 * Unified locale partial_order with class definition (cf. theory
   660 Orderings), added parameter ``less''.  INCOMPATIBILITY.
   661 
   662 * Constant "List.list_all2" in List.thy now uses authentic syntax.
   663 INCOMPATIBILITY: translations containing list_all2 may go wrong.  On
   664 Isar level, use abbreviations instead.
   665 
   666 * Renamed constant "List.op mem" to "List.memberl" INCOMPATIBILITY:
   667 rarely occuring name references (e.g. ``List.op mem.simps'') require
   668 renaming (e.g. ``List.memberl.simps'').
   669 
   670 * Renamed constants "0" to "HOL.zero" and "1" to "HOL.one".
   671 INCOMPATIBILITY.
   672 
   673 * Added theory Code_Generator providing class 'eq', allowing for code
   674 generation with polymorphic equality.
   675 
   676 * Numeral syntax: type 'bin' which was a mere type copy of 'int' has
   677 been abandoned in favour of plain 'int'. INCOMPATIBILITY --
   678 significant changes for setting up numeral syntax for types:
   679 
   680   - new constants Numeral.pred and Numeral.succ instead
   681       of former Numeral.bin_pred and Numeral.bin_succ.
   682   - Use integer operations instead of bin_add, bin_mult and so on.
   683   - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
   684   - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
   685 
   686 See HOL/Integ/IntArith.thy for an example setup.
   687 
   688 * New top level command 'normal_form' computes the normal form of a
   689 term that may contain free variables. For example ``normal_form
   690 "rev[a,b,c]"'' produces ``[b,c,a]'' (without proof).  This command is
   691 suitable for heavy-duty computations because the functions are
   692 compiled to ML first.
   693 
   694 * Alternative iff syntax "A <-> B" for equality on bool (with priority
   695 25 like -->); output depends on the "iff" print_mode, the default is
   696 "A = B" (with priority 50).
   697 
   698 * Renamed constants in HOL.thy and Orderings.thy:
   699     op +   ~> HOL.plus
   700     op -   ~> HOL.minus
   701     uminus ~> HOL.uminus
   702     op *   ~> HOL.times
   703     op <   ~> Orderings.less
   704     op <=  ~> Orderings.less_eq
   705 
   706 Adaptions may be required in the following cases:
   707 
   708 a) User-defined constants using any of the names "plus", "minus", "times",
   709 "less" or "less_eq". The standard syntax translations for "+", "-" and "*"
   710 may go wrong.
   711 INCOMPATIBILITY: use more specific names.
   712 
   713 b) Variables named "plus", "minus", "times", "less", "less_eq"
   714 INCOMPATIBILITY: use more specific names.
   715 
   716 c) Permutative equations (e.g. "a + b = b + a")
   717 Since the change of names also changes the order of terms, permutative
   718 rewrite rules may get applied in a different order. Experience shows that
   719 this is rarely the case (only two adaptions in the whole Isabelle
   720 distribution).
   721 INCOMPATIBILITY: rewrite proofs
   722 
   723 d) ML code directly refering to constant names
   724 This in general only affects hand-written proof tactics, simprocs and so on.
   725 INCOMPATIBILITY: grep your sourcecode and replace names.
   726 
   727 * Relations less (<) and less_eq (<=) are also available on type bool.
   728 Modified syntax to disallow nesting without explicit parentheses,
   729 e.g. "(x < y) < z" or "x < (y < z)", but NOT "x < y < z".
   730 
   731 * "LEAST x:A. P" expands to "LEAST x. x:A & P" (input only).
   732 
   733 * Relation composition operator "op O" now has precedence 75 and binds
   734 stronger than union and intersection. INCOMPATIBILITY.
   735 
   736 * The old set interval syntax "{m..n(}" (and relatives) has been
   737 removed.  Use "{m..<n}" (and relatives) instead.
   738 
   739 * In the context of the assumption "~(s = t)" the Simplifier rewrites
   740 "t = s" to False (by simproc "neq_simproc").  For backward
   741 compatibility this can be disabled by ML "reset use_neq_simproc".
   742 
   743 * "m dvd n" where m and n are numbers is evaluated to True/False by
   744 simp.
   745 
   746 * Theorem Cons_eq_map_conv no longer declared as ``simp''.
   747 
   748 * Theorem setsum_mult renamed to setsum_right_distrib.
   749 
   750 * Prefer ex1I over ex_ex1I in single-step reasoning, e.g. by the
   751 ``rule'' method.
   752 
   753 * Reimplemented methods ``sat'' and ``satx'', with several
   754 improvements: goals no longer need to be stated as "<prems> ==>
   755 False", equivalences (i.e. "=" on type bool) are handled, variable
   756 names of the form "lit_<n>" are no longer reserved, significant
   757 speedup.
   758 
   759 * Methods ``sat'' and ``satx'' can now replay MiniSat proof traces.
   760 zChaff is still supported as well.
   761 
   762 * 'inductive' and 'datatype': provide projections of mutual rules,
   763 bundled as foo_bar.inducts;
   764 
   765 * Library: moved theories Parity, GCD, Binomial, Infinite_Set to
   766 Library.
   767 
   768 * Library: moved theory Accessible_Part to main HOL.
   769 
   770 * Library: added theory Coinductive_List of potentially infinite lists
   771 as greatest fixed-point.
   772 
   773 * Library: added theory AssocList which implements (finite) maps as
   774 association lists.
   775 
   776 * Added proof method ``evaluation'' for efficiently solving a goal
   777 (i.e. a boolean expression) by compiling it to ML. The goal is
   778 "proved" (via an oracle) if it evaluates to True.
   779 
   780 * Linear arithmetic now splits certain operators (e.g. min, max, abs)
   781 also when invoked by the simplifier.  This results in the simplifier
   782 being more powerful on arithmetic goals.  INCOMPATIBILITY.  Set
   783 fast_arith_split_limit to 0 to obtain the old behavior.
   784 
   785 * Support for hex (0x20) and binary (0b1001) numerals.
   786 
   787 * New method: reify eqs (t), where eqs are equations for an
   788 interpretation I :: 'a list => 'b => 'c and t::'c is an optional
   789 parameter, computes a term s::'b and a list xs::'a list and proves the
   790 theorem I xs s = t. This is also known as reification or quoting. The
   791 resulting theorem is applied to the subgoal to substitute t with I xs
   792 s.  If t is omitted, the subgoal itself is reified.
   793 
   794 * New method: reflection corr_thm eqs (t). The parameters eqs and (t)
   795 are as explained above. corr_thm is a theorem for I vs (f t) = I vs t,
   796 where f is supposed to be a computable function (in the sense of code
   797 generattion). The method uses reify to compute s and xs as above then
   798 applies corr_thm and uses normalization by evaluation to "prove" f s =
   799 r and finally gets the theorem t = r, which is again applied to the
   800 subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
   801 
   802 * Reflection: Automatic refification now handels binding, an example
   803 is available in HOL/ex/ReflectionEx.thy
   804 
   805 
   806 *** HOL-Algebra ***
   807 
   808 * Formalisation of ideals and the quotient construction over rings.
   809 
   810 * Order and lattice theory no longer based on records.
   811 INCOMPATIBILITY.
   812 
   813 * Renamed lemmas least_carrier -> least_closed and greatest_carrier ->
   814 greatest_closed.  INCOMPATIBILITY.
   815 
   816 * Method algebra is now set up via an attribute.  For examples see
   817 Ring.thy.  INCOMPATIBILITY: the method is now weaker on combinations
   818 of algebraic structures.
   819 
   820 * Renamed theory CRing to Ring.
   821 
   822 
   823 *** HOL-Complex ***
   824 
   825 * Theory Real: new method ferrack implements quantifier elimination
   826 for linear arithmetic over the reals. The quantifier elimination
   827 feature is used only for decision, for compatibility with arith. This
   828 means a goal is either solved or left unchanged, no simplification.
   829 
   830 * Real: New axiomatic classes formalize real normed vector spaces and
   831 algebras, using new overloaded constants scaleR :: real => 'a => 'a
   832 and norm :: 'a => real.
   833 
   834 * Real: New constant of_real :: real => 'a::real_algebra_1 injects
   835 from reals into other types. The overloaded constant Reals :: 'a set
   836 is now defined as range of_real; potential INCOMPATIBILITY.
   837 
   838 * Hyperreal: Several constants that previously worked only for the
   839 reals have been generalized, so they now work over arbitrary vector
   840 spaces. Type annotations may need to be added in some cases; potential
   841 INCOMPATIBILITY.
   842 
   843   Infinitesimal  :: ('a::real_normed_vector) star set"
   844   HFinite        :: ('a::real_normed_vector) star set"
   845   HInfinite      :: ('a::real_normed_vector) star set"
   846   approx         :: ('a::real_normed_vector) star => 'a star => bool
   847   monad          :: ('a::real_normed_vector) star => 'a star set
   848   galaxy         :: ('a::real_normed_vector) star => 'a star set
   849   (NS)LIMSEQ     :: [nat, 'a::real_normed_vector, 'a] => bool
   850   (NS)convergent :: (nat => 'a::real_normed_vector) => bool
   851   (NS)Bseq       :: (nat => 'a::real_normed_vector) => bool
   852   (NS)Cauchy     :: (nat => 'a::real_normed_vector) => bool
   853   (NS)LIM        :: ['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool
   854   is(NS)Cont     :: ['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool
   855   deriv          :: ['a::real_normed_field => 'a, 'a, 'a] => bool
   856 
   857 * Complex: Some complex-specific constants are now abbreviations for
   858 overloaded ones: complex_of_real = of_real, cmod = norm, hcmod =
   859 hnorm.  Other constants have been entirely removed in favor of the
   860 polymorphic versions (INCOMPATIBILITY):
   861 
   862   approx        <-- capprox
   863   HFinite       <-- CFinite
   864   HInfinite     <-- CInfinite
   865   Infinitesimal <-- CInfinitesimal
   866   monad         <-- cmonad
   867   galaxy        <-- cgalaxy
   868   (NS)LIM       <-- (NS)CLIM, (NS)CRLIM
   869   is(NS)Cont    <-- is(NS)Contc, is(NS)contCR
   870   (ns)deriv     <-- (ns)cderiv
   871 
   872 
   873 *** ML ***
   874 
   875 * ML within Isar: antiquotations allow to embed statically-checked
   876 formal entities in the source, referring to the context available at
   877 compile-time.  For example:
   878 
   879 ML {* @{typ "'a => 'b"} *}
   880 ML {* @{term "%x. x"} *}
   881 ML {* @{prop "x == y"} *}
   882 ML {* @{ctyp "'a => 'b"} *}
   883 ML {* @{cterm "%x. x"} *}
   884 ML {* @{cprop "x == y"} *}
   885 ML {* @{thm asm_rl} *}
   886 ML {* @{thms asm_rl} *}
   887 ML {* @{const_name c} *}
   888 ML {* @{const_syntax c} *}
   889 ML {* @{context} *}
   890 ML {* @{theory} *}
   891 ML {* @{theory Pure} *}
   892 ML {* @{simpset} *}
   893 ML {* @{claset} *}
   894 ML {* @{clasimpset} *}
   895 
   896 The same works for sources being ``used'' within an Isar context.
   897 
   898 * ML in Isar: improved error reporting; extra verbosity with
   899 Toplevel.debug enabled.
   900 
   901 * Pure/library:
   902 
   903   val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
   904   val fold_burrow: ('a list -> 'c -> 'b list * 'd) -> 'a list list -> 'c -> 'b list list * 'd
   905 
   906 The semantics of "burrow" is: "take a function with *simulatanously*
   907 transforms a list of value, and apply it *simulatanously* to a list of
   908 list of values of the appropriate type". Compare this with "map" which
   909 would *not* apply its argument function simulatanously but in
   910 sequence; "fold_burrow" has an additional context.
   911 
   912 * Pure/library: functions map2 and fold2 with curried syntax for
   913 simultanous mapping and folding:
   914 
   915     val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   916     val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   917 
   918 * Pure/library: indexed lists - some functions in the Isabelle library
   919 treating lists over 'a as finite mappings from [0...n] to 'a have been
   920 given more convenient names and signatures reminiscent of similar
   921 functions for alists, tables, etc:
   922 
   923   val nth: 'a list -> int -> 'a 
   924   val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   925   val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   926 
   927 Note that fold_index starts counting at index 0, not 1 like foldln
   928 used to.
   929 
   930 * Pure/library: added general ``divide_and_conquer'' combinator on
   931 lists.
   932 
   933 * Pure/General/table.ML: the join operations now works via exceptions
   934 DUP/SAME instead of type option.  This is simpler in simple cases, and
   935 admits slightly more efficient complex applications.
   936 
   937 * Pure: datatype Context.generic joins theory/Proof.context and
   938 provides some facilities for code that works in either kind of
   939 context, notably GenericDataFun for uniform theory and proof data.
   940 
   941 * Pure: 'advanced' translation functions (parse_translation etc.) now
   942 use Context.generic instead of just theory.
   943 
   944 * Pure: simplified internal attribute type, which is now always
   945 Context.generic * thm -> Context.generic * thm.  Global (theory)
   946 vs. local (Proof.context) attributes have been discontinued, while
   947 minimizing code duplication.  Thm.rule_attribute and
   948 Thm.declaration_attribute build canonical attributes; see also
   949 structure Context for further operations on Context.generic, notably
   950 GenericDataFun.  INCOMPATIBILITY, need to adapt attribute type
   951 declarations and definitions.
   952 
   953 * Pure/kernel: consts certification ignores sort constraints given in
   954 signature declarations.  (This information is not relevant to the
   955 logic, but only for type inference.)  IMPORTANT INTERNAL CHANGE,
   956 potential INCOMPATIBILITY.
   957 
   958 * Pure: axiomatic type classes are now purely definitional, with
   959 explicit proofs of class axioms and super class relations performed
   960 internally.  See Pure/axclass.ML for the main internal interfaces --
   961 notably AxClass.define_class supercedes AxClass.add_axclass, and
   962 AxClass.axiomatize_class/classrel/arity supercede
   963 Sign.add_classes/classrel/arities.
   964 
   965 * Pure/Isar: Args/Attrib parsers operate on Context.generic --
   966 global/local versions on theory vs. Proof.context have been
   967 discontinued; Attrib.syntax and Method.syntax have been adapted
   968 accordingly.  INCOMPATIBILITY, need to adapt parser expressions for
   969 attributes, methods, etc.
   970 
   971 * Pure: several functions of signature "... -> theory -> theory * ..."
   972 have been reoriented to "... -> theory -> ... * theory" in order to
   973 allow natural usage in combination with the ||>, ||>>, |-> and
   974 fold_map combinators.
   975 
   976 * Pure: official theorem names (closed derivations) and additional
   977 comments (tags) are now strictly separate.  Name hints -- which are
   978 maintained as tags -- may be attached any time without affecting the
   979 derivation.
   980 
   981 * Pure: primitive rule lift_rule now takes goal cterm instead of an
   982 actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
   983 achieve the old behaviour.
   984 
   985 * Pure: the "Goal" constant is now called "prop", supporting a
   986 slightly more general idea of ``protecting'' meta-level rule
   987 statements.
   988 
   989 * Pure: Logic.(un)varify only works in a global context, which is now
   990 enforced instead of silently assumed.  INCOMPATIBILITY, may use
   991 Logic.legacy_(un)varify as temporary workaround.
   992 
   993 * Pure: structure Name provides scalable operations for generating
   994 internal variable names, notably Name.variants etc.  This replaces
   995 some popular functions from term.ML:
   996 
   997   Term.variant		->  Name.variant
   998   Term.variantlist	->  Name.variant_list  (*canonical argument order*)
   999   Term.invent_names	->  Name.invent_list
  1000 
  1001 Note that low-level renaming rarely occurs in new code -- operations
  1002 from structure Variable are used instead (see below).
  1003 
  1004 * Pure: structure Variable provides fundamental operations for proper
  1005 treatment of fixed/schematic variables in a context.  For example,
  1006 Variable.import introduces fixes for schematics of given facts and
  1007 Variable.export reverses the effect (up to renaming) -- this replaces
  1008 various freeze_thaw operations.
  1009 
  1010 * Pure: structure Goal provides simple interfaces for
  1011 init/conclude/finish and tactical prove operations (replacing former
  1012 Tactic.prove).  Goal.prove is the canonical way to prove results
  1013 within a given context; Goal.prove_global is a degraded version for
  1014 theory level goals, including a global Drule.standard.  Note that
  1015 OldGoals.prove_goalw_cterm has long been obsolete, since it is
  1016 ill-behaved in a local proof context (e.g. with local fixes/assumes or
  1017 in a locale context).
  1018 
  1019 * Isar: simplified treatment of user-level errors, using exception
  1020 ERROR of string uniformly.  Function error now merely raises ERROR,
  1021 without any side effect on output channels.  The Isar toplevel takes
  1022 care of proper display of ERROR exceptions.  ML code may use plain
  1023 handle/can/try; cat_error may be used to concatenate errors like this:
  1024 
  1025   ... handle ERROR msg => cat_error msg "..."
  1026 
  1027 Toplevel ML code (run directly or through the Isar toplevel) may be
  1028 embedded into the Isar toplevel with exception display/debug like
  1029 this:
  1030 
  1031   Isar.toplevel (fn () => ...)
  1032 
  1033 INCOMPATIBILITY, removed special transform_error facilities, removed
  1034 obsolete variants of user-level exceptions (ERROR_MESSAGE,
  1035 Context.PROOF, ProofContext.CONTEXT, Proof.STATE, ProofHistory.FAIL)
  1036 -- use plain ERROR instead.
  1037 
  1038 * Isar: theory setup now has type (theory -> theory), instead of a
  1039 list.  INCOMPATIBILITY, may use #> to compose setup functions.
  1040 
  1041 * Isar: installed ML toplevel pretty printer for type Proof.context,
  1042 subject to ProofContext.debug/verbose flags.
  1043 
  1044 * Isar: Toplevel.theory_to_proof admits transactions that modify the
  1045 theory before entering a proof state.  Transactions now always see a
  1046 quasi-functional intermediate checkpoint, both in interactive and
  1047 batch mode.
  1048 
  1049 * Simplifier: the simpset of a running simplification process now
  1050 contains a proof context (cf. Simplifier.the_context), which is the
  1051 very context that the initial simpset has been retrieved from (by
  1052 simpset_of/local_simpset_of).  Consequently, all plug-in components
  1053 (solver, looper etc.) may depend on arbitrary proof data.
  1054 
  1055 * Simplifier.inherit_context inherits the proof context (plus the
  1056 local bounds) of the current simplification process; any simproc
  1057 etc. that calls the Simplifier recursively should do this!  Removed
  1058 former Simplifier.inherit_bounds, which is already included here --
  1059 INCOMPATIBILITY.  Tools based on low-level rewriting may even have to
  1060 specify an explicit context using Simplifier.context/theory_context.
  1061 
  1062 * Simplifier/Classical Reasoner: more abstract interfaces
  1063 change_simpset/claset for modifying the simpset/claset reference of a
  1064 theory; raw versions simpset/claset_ref etc. have been discontinued --
  1065 INCOMPATIBILITY.
  1066 
  1067 * Provers: more generic wrt. syntax of object-logics, avoid hardwired
  1068 "Trueprop" etc.
  1069 
  1070 
  1071 *** System ***
  1072 
  1073 * settings: ML_IDENTIFIER -- which is appended to user specific heap
  1074 locations -- now includes the Isabelle version identifier as well.
  1075 This simplifies use of multiple Isabelle installations.
  1076 
  1077 * isabelle-process: option -S (secure mode) disables some critical
  1078 operations, notably runtime compilation and evaluation of ML source
  1079 code.
  1080 
  1081 
  1082 New in Isabelle2005 (October 2005)
  1083 ----------------------------------
  1084 
  1085 *** General ***
  1086 
  1087 * Theory headers: the new header syntax for Isar theories is
  1088 
  1089   theory <name>
  1090   imports <theory1> ... <theoryN>
  1091   uses <file1> ... <fileM>
  1092   begin
  1093 
  1094 where the 'uses' part is optional.  The previous syntax
  1095 
  1096   theory <name> = <theory1> + ... + <theoryN>:
  1097 
  1098 will disappear in the next release.  Use isatool fixheaders to convert
  1099 existing theory files.  Note that there is no change in ancient
  1100 non-Isar theories now, but these will disappear soon.
  1101 
  1102 * Theory loader: parent theories can now also be referred to via
  1103 relative and absolute paths.
  1104 
  1105 * Command 'find_theorems' searches for a list of criteria instead of a
  1106 list of constants. Known criteria are: intro, elim, dest, name:string,
  1107 simp:term, and any term. Criteria can be preceded by '-' to select
  1108 theorems that do not match. Intro, elim, dest select theorems that
  1109 match the current goal, name:s selects theorems whose fully qualified
  1110 name contain s, and simp:term selects all simplification rules whose
  1111 lhs match term.  Any other term is interpreted as pattern and selects
  1112 all theorems matching the pattern. Available in ProofGeneral under
  1113 'ProofGeneral -> Find Theorems' or C-c C-f.  Example:
  1114 
  1115   C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL."
  1116 
  1117 prints the last 100 theorems matching the pattern "(_::nat) + _ + _",
  1118 matching the current goal as introduction rule and not having "HOL."
  1119 in their name (i.e. not being defined in theory HOL).
  1120 
  1121 * Command 'thms_containing' has been discontinued in favour of
  1122 'find_theorems'; INCOMPATIBILITY.
  1123 
  1124 * Communication with Proof General is now 8bit clean, which means that
  1125 Unicode text in UTF-8 encoding may be used within theory texts (both
  1126 formal and informal parts).  Cf. option -U of the Isabelle Proof
  1127 General interface.  Here are some simple examples (cf. src/HOL/ex):
  1128 
  1129   http://isabelle.in.tum.de/library/HOL/ex/Hebrew.html
  1130   http://isabelle.in.tum.de/library/HOL/ex/Chinese.html
  1131 
  1132 * Improved efficiency of the Simplifier and, to a lesser degree, the
  1133 Classical Reasoner.  Typical big applications run around 2 times
  1134 faster.
  1135 
  1136 
  1137 *** Document preparation ***
  1138 
  1139 * Commands 'display_drafts' and 'print_drafts' perform simple output
  1140 of raw sources.  Only those symbols that do not require additional
  1141 LaTeX packages (depending on comments in isabellesym.sty) are
  1142 displayed properly, everything else is left verbatim.  isatool display
  1143 and isatool print are used as front ends (these are subject to the
  1144 DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
  1145 
  1146 * Command tags control specific markup of certain regions of text,
  1147 notably folding and hiding.  Predefined tags include "theory" (for
  1148 theory begin and end), "proof" for proof commands, and "ML" for
  1149 commands involving ML code; the additional tags "visible" and
  1150 "invisible" are unused by default.  Users may give explicit tag
  1151 specifications in the text, e.g. ''by %invisible (auto)''.  The
  1152 interpretation of tags is determined by the LaTeX job during document
  1153 preparation: see option -V of isatool usedir, or options -n and -t of
  1154 isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
  1155 \isadroptag.
  1156 
  1157 Several document versions may be produced at the same time via isatool
  1158 usedir (the generated index.html will link all of them).  Typical
  1159 specifications include ''-V document=theory,proof,ML'' to present
  1160 theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
  1161 proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
  1162 these parts without any formal replacement text.  The Isabelle site
  1163 default settings produce ''document'' and ''outline'' versions as
  1164 specified above.
  1165 
  1166 * Several new antiquotations:
  1167 
  1168   @{term_type term} prints a term with its type annotated;
  1169 
  1170   @{typeof term} prints the type of a term;
  1171 
  1172   @{const const} is the same as @{term const}, but checks that the
  1173   argument is a known logical constant;
  1174 
  1175   @{term_style style term} and @{thm_style style thm} print a term or
  1176   theorem applying a "style" to it
  1177 
  1178   @{ML text}
  1179 
  1180 Predefined styles are 'lhs' and 'rhs' printing the lhs/rhs of
  1181 definitions, equations, inequations etc., 'concl' printing only the
  1182 conclusion of a meta-logical statement theorem, and 'prem1' .. 'prem19'
  1183 to print the specified premise.  TermStyle.add_style provides an ML
  1184 interface for introducing further styles.  See also the "LaTeX Sugar"
  1185 document practical applications.  The ML antiquotation prints
  1186 type-checked ML expressions verbatim.
  1187 
  1188 * Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
  1189 and 'text' support optional locale specification '(in loc)', which
  1190 specifies the default context for interpreting antiquotations.  For
  1191 example: 'text (in lattice) {* @{thm inf_assoc}*}'.
  1192 
  1193 * Option 'locale=NAME' of antiquotations specifies an alternative
  1194 context interpreting the subsequent argument.  For example: @{thm
  1195 [locale=lattice] inf_assoc}.
  1196 
  1197 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
  1198 a proof context.
  1199 
  1200 * Proper output of antiquotations for theory commands involving a
  1201 proof context (such as 'locale' or 'theorem (in loc) ...').
  1202 
  1203 * Delimiters of outer tokens (string etc.) now produce separate LaTeX
  1204 macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
  1205 
  1206 * isatool usedir: new option -C (default true) controls whether option
  1207 -D should include a copy of the original document directory; -C false
  1208 prevents unwanted effects such as copying of administrative CVS data.
  1209 
  1210 
  1211 *** Pure ***
  1212 
  1213 * Considerably improved version of 'constdefs' command.  Now performs
  1214 automatic type-inference of declared constants; additional support for
  1215 local structure declarations (cf. locales and HOL records), see also
  1216 isar-ref manual.  Potential INCOMPATIBILITY: need to observe strictly
  1217 sequential dependencies of definitions within a single 'constdefs'
  1218 section; moreover, the declared name needs to be an identifier.  If
  1219 all fails, consider to fall back on 'consts' and 'defs' separately.
  1220 
  1221 * Improved indexed syntax and implicit structures.  First of all,
  1222 indexed syntax provides a notational device for subscripted
  1223 application, using the new syntax \<^bsub>term\<^esub> for arbitrary
  1224 expressions.  Secondly, in a local context with structure
  1225 declarations, number indexes \<^sub>n or the empty index (default
  1226 number 1) refer to a certain fixed variable implicitly; option
  1227 show_structs controls printing of implicit structures.  Typical
  1228 applications of these concepts involve record types and locales.
  1229 
  1230 * New command 'no_syntax' removes grammar declarations (and
  1231 translations) resulting from the given syntax specification, which is
  1232 interpreted in the same manner as for the 'syntax' command.
  1233 
  1234 * 'Advanced' translation functions (parse_translation etc.) may depend
  1235 on the signature of the theory context being presently used for
  1236 parsing/printing, see also isar-ref manual.
  1237 
  1238 * Improved 'oracle' command provides a type-safe interface to turn an
  1239 ML expression of type theory -> T -> term into a primitive rule of
  1240 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
  1241 is already included here); see also FOL/ex/IffExample.thy;
  1242 INCOMPATIBILITY.
  1243 
  1244 * axclass: name space prefix for class "c" is now "c_class" (was "c"
  1245 before); "cI" is no longer bound, use "c.intro" instead.
  1246 INCOMPATIBILITY.  This change avoids clashes of fact bindings for
  1247 axclasses vs. locales.
  1248 
  1249 * Improved internal renaming of symbolic identifiers -- attach primes
  1250 instead of base 26 numbers.
  1251 
  1252 * New flag show_question_marks controls printing of leading question
  1253 marks in schematic variable names.
  1254 
  1255 * In schematic variable names, *any* symbol following \<^isub> or
  1256 \<^isup> is now treated as part of the base name.  For example, the
  1257 following works without printing of awkward ".0" indexes:
  1258 
  1259   lemma "x\<^isub>1 = x\<^isub>2 ==> x\<^isub>2 = x\<^isub>1"
  1260     by simp
  1261 
  1262 * Inner syntax includes (*(*nested*) comments*).
  1263 
  1264 * Pretty printer now supports unbreakable blocks, specified in mixfix
  1265 annotations as "(00...)".
  1266 
  1267 * Clear separation of logical types and nonterminals, where the latter
  1268 may only occur in 'syntax' specifications or type abbreviations.
  1269 Before that distinction was only partially implemented via type class
  1270 "logic" vs. "{}".  Potential INCOMPATIBILITY in rare cases of improper
  1271 use of 'types'/'consts' instead of 'nonterminals'/'syntax'.  Some very
  1272 exotic syntax specifications may require further adaption
  1273 (e.g. Cube/Cube.thy).
  1274 
  1275 * Removed obsolete type class "logic", use the top sort {} instead.
  1276 Note that non-logical types should be declared as 'nonterminals'
  1277 rather than 'types'.  INCOMPATIBILITY for new object-logic
  1278 specifications.
  1279 
  1280 * Attributes 'induct' and 'cases': type or set names may now be
  1281 locally fixed variables as well.
  1282 
  1283 * Simplifier: can now control the depth to which conditional rewriting
  1284 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
  1285 Limit.
  1286 
  1287 * Simplifier: simplification procedures may now take the current
  1288 simpset into account (cf. Simplifier.simproc(_i) / mk_simproc
  1289 interface), which is very useful for calling the Simplifier
  1290 recursively.  Minor INCOMPATIBILITY: the 'prems' argument of simprocs
  1291 is gone -- use prems_of_ss on the simpset instead.  Moreover, the
  1292 low-level mk_simproc no longer applies Logic.varify internally, to
  1293 allow for use in a context of fixed variables.
  1294 
  1295 * thin_tac now works even if the assumption being deleted contains !!
  1296 or ==>.  More generally, erule now works even if the major premise of
  1297 the elimination rule contains !! or ==>.
  1298 
  1299 * Method 'rules' has been renamed to 'iprover'. INCOMPATIBILITY.
  1300 
  1301 * Reorganized bootstrapping of the Pure theories; CPure is now derived
  1302 from Pure, which contains all common declarations already.  Both
  1303 theories are defined via plain Isabelle/Isar .thy files.
  1304 INCOMPATIBILITY: elements of CPure (such as the CPure.intro /
  1305 CPure.elim / CPure.dest attributes) now appear in the Pure name space;
  1306 use isatool fixcpure to adapt your theory and ML sources.
  1307 
  1308 * New syntax 'name(i-j, i-, i, ...)' for referring to specific
  1309 selections of theorems in named facts via index ranges.
  1310 
  1311 * 'print_theorems': in theory mode, really print the difference
  1312 wrt. the last state (works for interactive theory development only),
  1313 in proof mode print all local facts (cf. 'print_facts');
  1314 
  1315 * 'hide': option '(open)' hides only base names.
  1316 
  1317 * More efficient treatment of intermediate checkpoints in interactive
  1318 theory development.
  1319 
  1320 * Code generator is now invoked via code_module (incremental code
  1321 generation) and code_library (modular code generation, ML structures
  1322 for each theory).  INCOMPATIBILITY: new keywords 'file' and 'contains'
  1323 must be quoted when used as identifiers.
  1324 
  1325 * New 'value' command for reading, evaluating and printing terms using
  1326 the code generator.  INCOMPATIBILITY: command keyword 'value' must be
  1327 quoted when used as identifier.
  1328 
  1329 
  1330 *** Locales ***
  1331 
  1332 * New commands for the interpretation of locale expressions in
  1333 theories (1), locales (2) and proof contexts (3).  These generate
  1334 proof obligations from the expression specification.  After the
  1335 obligations have been discharged, theorems of the expression are added
  1336 to the theory, target locale or proof context.  The synopsis of the
  1337 commands is a follows:
  1338 
  1339   (1) interpretation expr inst
  1340   (2) interpretation target < expr
  1341   (3) interpret expr inst
  1342 
  1343 Interpretation in theories and proof contexts require a parameter
  1344 instantiation of terms from the current context.  This is applied to
  1345 specifications and theorems of the interpreted expression.
  1346 Interpretation in locales only permits parameter renaming through the
  1347 locale expression.  Interpretation is smart in that interpretations
  1348 that are active already do not occur in proof obligations, neither are
  1349 instantiated theorems stored in duplicate.  Use 'print_interps' to
  1350 inspect active interpretations of a particular locale.  For details,
  1351 see the Isar Reference manual.  Examples can be found in
  1352 HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy.
  1353 
  1354 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
  1355 'interpret' instead.
  1356 
  1357 * New context element 'constrains' for adding type constraints to
  1358 parameters.
  1359 
  1360 * Context expressions: renaming of parameters with syntax
  1361 redeclaration.
  1362 
  1363 * Locale declaration: 'includes' disallowed.
  1364 
  1365 * Proper static binding of attribute syntax -- i.e. types / terms /
  1366 facts mentioned as arguments are always those of the locale definition
  1367 context, independently of the context of later invocations.  Moreover,
  1368 locale operations (renaming and type / term instantiation) are applied
  1369 to attribute arguments as expected.
  1370 
  1371 INCOMPATIBILITY of the ML interface: always pass Attrib.src instead of
  1372 actual attributes; rare situations may require Attrib.attribute to
  1373 embed those attributes into Attrib.src that lack concrete syntax.
  1374 Attribute implementations need to cooperate properly with the static
  1375 binding mechanism.  Basic parsers Args.XXX_typ/term/prop and
  1376 Attrib.XXX_thm etc. already do the right thing without further
  1377 intervention.  Only unusual applications -- such as "where" or "of"
  1378 (cf. src/Pure/Isar/attrib.ML), which process arguments depending both
  1379 on the context and the facts involved -- may have to assign parsed
  1380 values to argument tokens explicitly.
  1381 
  1382 * Changed parameter management in theorem generation for long goal
  1383 statements with 'includes'.  INCOMPATIBILITY: produces a different
  1384 theorem statement in rare situations.
  1385 
  1386 * Locale inspection command 'print_locale' omits notes elements.  Use
  1387 'print_locale!' to have them included in the output.
  1388 
  1389 
  1390 *** Provers ***
  1391 
  1392 * Provers/hypsubst.ML: improved version of the subst method, for
  1393 single-step rewriting: it now works in bound variable contexts. New is
  1394 'subst (asm)', for rewriting an assumption.  INCOMPATIBILITY: may
  1395 rewrite a different subterm than the original subst method, which is
  1396 still available as 'simplesubst'.
  1397 
  1398 * Provers/quasi.ML: new transitivity reasoners for transitivity only
  1399 and quasi orders.
  1400 
  1401 * Provers/trancl.ML: new transitivity reasoner for transitive and
  1402 reflexive-transitive closure of relations.
  1403 
  1404 * Provers/blast.ML: new reference depth_limit to make blast's depth
  1405 limit (previously hard-coded with a value of 20) user-definable.
  1406 
  1407 * Provers/simplifier.ML has been moved to Pure, where Simplifier.setup
  1408 is peformed already.  Object-logics merely need to finish their
  1409 initial simpset configuration as before.  INCOMPATIBILITY.
  1410 
  1411 
  1412 *** HOL ***
  1413 
  1414 * Symbolic syntax of Hilbert Choice Operator is now as follows:
  1415 
  1416   syntax (epsilon)
  1417     "_Eps" :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
  1418 
  1419 The symbol \<some> is displayed as the alternative epsilon of LaTeX
  1420 and x-symbol; use option '-m epsilon' to get it actually printed.
  1421 Moreover, the mathematically important symbolic identifier \<epsilon>
  1422 becomes available as variable, constant etc.  INCOMPATIBILITY,
  1423 
  1424 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
  1425 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
  1426 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to
  1427 support corresponding Isar calculations.
  1428 
  1429 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
  1430 instead of ":".
  1431 
  1432 * theory SetInterval: changed the syntax for open intervals:
  1433 
  1434   Old       New
  1435   {..n(}    {..<n}
  1436   {)n..}    {n<..}
  1437   {m..n(}   {m..<n}
  1438   {)m..n}   {m<..n}
  1439   {)m..n(}  {m<..<n}
  1440 
  1441 The old syntax is still supported but will disappear in the next
  1442 release.  For conversion use the following Emacs search and replace
  1443 patterns (these are not perfect but work quite well):
  1444 
  1445   {)\([^\.]*\)\.\.  ->  {\1<\.\.}
  1446   \.\.\([^(}]*\)(}  ->  \.\.<\1}
  1447 
  1448 * Theory Commutative_Ring (in Library): method comm_ring for proving
  1449 equalities in commutative rings; method 'algebra' provides a generic
  1450 interface.
  1451 
  1452 * Theory Finite_Set: changed the syntax for 'setsum', summation over
  1453 finite sets: "setsum (%x. e) A", which used to be "\<Sum>x:A. e", is
  1454 now either "SUM x:A. e" or "\<Sum>x \<in> A. e". The bound variable can
  1455 be a tuple pattern.
  1456 
  1457 Some new syntax forms are available:
  1458 
  1459   "\<Sum>x | P. e"      for     "setsum (%x. e) {x. P}"
  1460   "\<Sum>x = a..b. e"   for     "setsum (%x. e) {a..b}"
  1461   "\<Sum>x = a..<b. e"  for     "setsum (%x. e) {a..<b}"
  1462   "\<Sum>x < k. e"      for     "setsum (%x. e) {..<k}"
  1463 
  1464 The latter form "\<Sum>x < k. e" used to be based on a separate
  1465 function "Summation", which has been discontinued.
  1466 
  1467 * theory Finite_Set: in structured induction proofs, the insert case
  1468 is now 'case (insert x F)' instead of the old counterintuitive 'case
  1469 (insert F x)'.
  1470 
  1471 * The 'refute' command has been extended to support a much larger
  1472 fragment of HOL, including axiomatic type classes, constdefs and
  1473 typedefs, inductive datatypes and recursion.
  1474 
  1475 * New tactics 'sat' and 'satx' to prove propositional tautologies.
  1476 Requires zChaff with proof generation to be installed.  See
  1477 HOL/ex/SAT_Examples.thy for examples.
  1478 
  1479 * Datatype induction via method 'induct' now preserves the name of the
  1480 induction variable. For example, when proving P(xs::'a list) by
  1481 induction on xs, the induction step is now P(xs) ==> P(a#xs) rather
  1482 than P(list) ==> P(a#list) as previously.  Potential INCOMPATIBILITY
  1483 in unstructured proof scripts.
  1484 
  1485 * Reworked implementation of records.  Improved scalability for
  1486 records with many fields, avoiding performance problems for type
  1487 inference. Records are no longer composed of nested field types, but
  1488 of nested extension types. Therefore the record type only grows linear
  1489 in the number of extensions and not in the number of fields.  The
  1490 top-level (users) view on records is preserved.  Potential
  1491 INCOMPATIBILITY only in strange cases, where the theory depends on the
  1492 old record representation. The type generated for a record is called
  1493 <record_name>_ext_type.
  1494 
  1495 Flag record_quick_and_dirty_sensitive can be enabled to skip the
  1496 proofs triggered by a record definition or a simproc (if
  1497 quick_and_dirty is enabled).  Definitions of large records can take
  1498 quite long.
  1499 
  1500 New simproc record_upd_simproc for simplification of multiple record
  1501 updates enabled by default.  Moreover, trivial updates are also
  1502 removed: r(|x := x r|) = r.  INCOMPATIBILITY: old proofs break
  1503 occasionally, since simplification is more powerful by default.
  1504 
  1505 * typedef: proper support for polymorphic sets, which contain extra
  1506 type-variables in the term.
  1507 
  1508 * Simplifier: automatically reasons about transitivity chains
  1509 involving "trancl" (r^+) and "rtrancl" (r^*) by setting up tactics
  1510 provided by Provers/trancl.ML as additional solvers.  INCOMPATIBILITY:
  1511 old proofs break occasionally as simplification may now solve more
  1512 goals than previously.
  1513 
  1514 * Simplifier: converts x <= y into x = y if assumption y <= x is
  1515 present.  Works for all partial orders (class "order"), in particular
  1516 numbers and sets.  For linear orders (e.g. numbers) it treats ~ x < y
  1517 just like y <= x.
  1518 
  1519 * Simplifier: new simproc for "let x = a in f x".  If a is a free or
  1520 bound variable or a constant then the let is unfolded.  Otherwise
  1521 first a is simplified to b, and then f b is simplified to g. If
  1522 possible we abstract b from g arriving at "let x = b in h x",
  1523 otherwise we unfold the let and arrive at g.  The simproc can be
  1524 enabled/disabled by the reference use_let_simproc.  Potential
  1525 INCOMPATIBILITY since simplification is more powerful by default.
  1526 
  1527 * Classical reasoning: the meson method now accepts theorems as arguments.
  1528 
  1529 * Prover support: pre-release of the Isabelle-ATP linkup, which runs background
  1530 jobs to provide advice on the provability of subgoals.
  1531 
  1532 * Theory OrderedGroup and Ring_and_Field: various additions and
  1533 improvements to faciliate calculations involving equalities and
  1534 inequalities.
  1535 
  1536 The following theorems have been eliminated or modified
  1537 (INCOMPATIBILITY):
  1538 
  1539   abs_eq             now named abs_of_nonneg
  1540   abs_of_ge_0        now named abs_of_nonneg
  1541   abs_minus_eq       now named abs_of_nonpos
  1542   imp_abs_id         now named abs_of_nonneg
  1543   imp_abs_neg_id     now named abs_of_nonpos
  1544   mult_pos           now named mult_pos_pos
  1545   mult_pos_le        now named mult_nonneg_nonneg
  1546   mult_pos_neg_le    now named mult_nonneg_nonpos
  1547   mult_pos_neg2_le   now named mult_nonneg_nonpos2
  1548   mult_neg           now named mult_neg_neg
  1549   mult_neg_le        now named mult_nonpos_nonpos
  1550 
  1551 * Theory Parity: added rules for simplifying exponents.
  1552 
  1553 * Theory List:
  1554 
  1555 The following theorems have been eliminated or modified
  1556 (INCOMPATIBILITY):
  1557 
  1558   list_all_Nil       now named list_all.simps(1)
  1559   list_all_Cons      now named list_all.simps(2)
  1560   list_all_conv      now named list_all_iff
  1561   set_mem_eq         now named mem_iff
  1562 
  1563 * Theories SetsAndFunctions and BigO (see HOL/Library) support
  1564 asymptotic "big O" calculations.  See the notes in BigO.thy.
  1565 
  1566 
  1567 *** HOL-Complex ***
  1568 
  1569 * Theory RealDef: better support for embedding natural numbers and
  1570 integers in the reals.
  1571 
  1572 The following theorems have been eliminated or modified
  1573 (INCOMPATIBILITY):
  1574 
  1575   exp_ge_add_one_self  now requires no hypotheses
  1576   real_of_int_add      reversed direction of equality (use [symmetric])
  1577   real_of_int_minus    reversed direction of equality (use [symmetric])
  1578   real_of_int_diff     reversed direction of equality (use [symmetric])
  1579   real_of_int_mult     reversed direction of equality (use [symmetric])
  1580 
  1581 * Theory RComplete: expanded support for floor and ceiling functions.
  1582 
  1583 * Theory Ln is new, with properties of the natural logarithm
  1584 
  1585 * Hyperreal: There is a new type constructor "star" for making
  1586 nonstandard types.  The old type names are now type synonyms:
  1587 
  1588   hypreal = real star
  1589   hypnat = nat star
  1590   hcomplex = complex star
  1591 
  1592 * Hyperreal: Many groups of similarly-defined constants have been
  1593 replaced by polymorphic versions (INCOMPATIBILITY):
  1594 
  1595   star_of <-- hypreal_of_real, hypnat_of_nat, hcomplex_of_complex
  1596 
  1597   starset      <-- starsetNat, starsetC
  1598   *s*          <-- *sNat*, *sc*
  1599   starset_n    <-- starsetNat_n, starsetC_n
  1600   *sn*         <-- *sNatn*, *scn*
  1601   InternalSets <-- InternalNatSets, InternalCSets
  1602 
  1603   starfun      <-- starfun{Nat,Nat2,C,RC,CR}
  1604   *f*          <-- *fNat*, *fNat2*, *fc*, *fRc*, *fcR*
  1605   starfun_n    <-- starfun{Nat,Nat2,C,RC,CR}_n
  1606   *fn*         <-- *fNatn*, *fNat2n*, *fcn*, *fRcn*, *fcRn*
  1607   InternalFuns <-- InternalNatFuns, InternalNatFuns2, Internal{C,RC,CR}Funs
  1608 
  1609 * Hyperreal: Many type-specific theorems have been removed in favor of
  1610 theorems specific to various axiomatic type classes (INCOMPATIBILITY):
  1611 
  1612   add_commute <-- {hypreal,hypnat,hcomplex}_add_commute
  1613   add_assoc   <-- {hypreal,hypnat,hcomplex}_add_assocs
  1614   OrderedGroup.add_0 <-- {hypreal,hypnat,hcomplex}_add_zero_left
  1615   OrderedGroup.add_0_right <-- {hypreal,hcomplex}_add_zero_right
  1616   right_minus <-- hypreal_add_minus
  1617   left_minus <-- {hypreal,hcomplex}_add_minus_left
  1618   mult_commute <-- {hypreal,hypnat,hcomplex}_mult_commute
  1619   mult_assoc <-- {hypreal,hypnat,hcomplex}_mult_assoc
  1620   mult_1_left <-- {hypreal,hypnat}_mult_1, hcomplex_mult_one_left
  1621   mult_1_right <-- hcomplex_mult_one_right
  1622   mult_zero_left <-- hcomplex_mult_zero_left
  1623   left_distrib <-- {hypreal,hypnat,hcomplex}_add_mult_distrib
  1624   right_distrib <-- hypnat_add_mult_distrib2
  1625   zero_neq_one <-- {hypreal,hypnat,hcomplex}_zero_not_eq_one
  1626   right_inverse <-- hypreal_mult_inverse
  1627   left_inverse <-- hypreal_mult_inverse_left, hcomplex_mult_inv_left
  1628   order_refl <-- {hypreal,hypnat}_le_refl
  1629   order_trans <-- {hypreal,hypnat}_le_trans
  1630   order_antisym <-- {hypreal,hypnat}_le_anti_sym
  1631   order_less_le <-- {hypreal,hypnat}_less_le
  1632   linorder_linear <-- {hypreal,hypnat}_le_linear
  1633   add_left_mono <-- {hypreal,hypnat}_add_left_mono
  1634   mult_strict_left_mono <-- {hypreal,hypnat}_mult_less_mono2
  1635   add_nonneg_nonneg <-- hypreal_le_add_order
  1636 
  1637 * Hyperreal: Separate theorems having to do with type-specific
  1638 versions of constants have been merged into theorems that apply to the
  1639 new polymorphic constants (INCOMPATIBILITY):
  1640 
  1641   STAR_UNIV_set <-- {STAR_real,NatStar_real,STARC_complex}_set
  1642   STAR_empty_set <-- {STAR,NatStar,STARC}_empty_set
  1643   STAR_Un <-- {STAR,NatStar,STARC}_Un
  1644   STAR_Int <-- {STAR,NatStar,STARC}_Int
  1645   STAR_Compl <-- {STAR,NatStar,STARC}_Compl
  1646   STAR_subset <-- {STAR,NatStar,STARC}_subset
  1647   STAR_mem <-- {STAR,NatStar,STARC}_mem
  1648   STAR_mem_Compl <-- {STAR,STARC}_mem_Compl
  1649   STAR_diff <-- {STAR,STARC}_diff
  1650   STAR_star_of_image_subset <-- {STAR_hypreal_of_real, NatStar_hypreal_of_real,
  1651     STARC_hcomplex_of_complex}_image_subset
  1652   starset_n_Un <-- starset{Nat,C}_n_Un
  1653   starset_n_Int <-- starset{Nat,C}_n_Int
  1654   starset_n_Compl <-- starset{Nat,C}_n_Compl
  1655   starset_n_diff <-- starset{Nat,C}_n_diff
  1656   InternalSets_Un <-- Internal{Nat,C}Sets_Un
  1657   InternalSets_Int <-- Internal{Nat,C}Sets_Int
  1658   InternalSets_Compl <-- Internal{Nat,C}Sets_Compl
  1659   InternalSets_diff <-- Internal{Nat,C}Sets_diff
  1660   InternalSets_UNIV_diff <-- Internal{Nat,C}Sets_UNIV_diff
  1661   InternalSets_starset_n <-- Internal{Nat,C}Sets_starset{Nat,C}_n
  1662   starset_starset_n_eq <-- starset{Nat,C}_starset{Nat,C}_n_eq
  1663   starset_n_starset <-- starset{Nat,C}_n_starset{Nat,C}
  1664   starfun_n_starfun <-- starfun{Nat,Nat2,C,RC,CR}_n_starfun{Nat,Nat2,C,RC,CR}
  1665   starfun <-- starfun{Nat,Nat2,C,RC,CR}
  1666   starfun_mult <-- starfun{Nat,Nat2,C,RC,CR}_mult
  1667   starfun_add <-- starfun{Nat,Nat2,C,RC,CR}_add
  1668   starfun_minus <-- starfun{Nat,Nat2,C,RC,CR}_minus
  1669   starfun_diff <-- starfun{C,RC,CR}_diff
  1670   starfun_o <-- starfun{NatNat2,Nat2,_stafunNat,C,C_starfunRC,_starfunCR}_o
  1671   starfun_o2 <-- starfun{NatNat2,_stafunNat,C,C_starfunRC,_starfunCR}_o2
  1672   starfun_const_fun <-- starfun{Nat,Nat2,C,RC,CR}_const_fun
  1673   starfun_inverse <-- starfun{Nat,C,RC,CR}_inverse
  1674   starfun_eq <-- starfun{Nat,Nat2,C,RC,CR}_eq
  1675   starfun_eq_iff <-- starfun{C,RC,CR}_eq_iff
  1676   starfun_Id <-- starfunC_Id
  1677   starfun_approx <-- starfun{Nat,CR}_approx
  1678   starfun_capprox <-- starfun{C,RC}_capprox
  1679   starfun_abs <-- starfunNat_rabs
  1680   starfun_lambda_cancel <-- starfun{C,CR,RC}_lambda_cancel
  1681   starfun_lambda_cancel2 <-- starfun{C,CR,RC}_lambda_cancel2
  1682   starfun_mult_HFinite_approx <-- starfunCR_mult_HFinite_capprox
  1683   starfun_mult_CFinite_capprox <-- starfun{C,RC}_mult_CFinite_capprox
  1684   starfun_add_capprox <-- starfun{C,RC}_add_capprox
  1685   starfun_add_approx <-- starfunCR_add_approx
  1686   starfun_inverse_inverse <-- starfunC_inverse_inverse
  1687   starfun_divide <-- starfun{C,CR,RC}_divide
  1688   starfun_n <-- starfun{Nat,C}_n
  1689   starfun_n_mult <-- starfun{Nat,C}_n_mult
  1690   starfun_n_add <-- starfun{Nat,C}_n_add
  1691   starfun_n_add_minus <-- starfunNat_n_add_minus
  1692   starfun_n_const_fun <-- starfun{Nat,C}_n_const_fun
  1693   starfun_n_minus <-- starfun{Nat,C}_n_minus
  1694   starfun_n_eq <-- starfun{Nat,C}_n_eq
  1695 
  1696   star_n_add <-- {hypreal,hypnat,hcomplex}_add
  1697   star_n_minus <-- {hypreal,hcomplex}_minus
  1698   star_n_diff <-- {hypreal,hcomplex}_diff
  1699   star_n_mult <-- {hypreal,hcomplex}_mult
  1700   star_n_inverse <-- {hypreal,hcomplex}_inverse
  1701   star_n_le <-- {hypreal,hypnat}_le
  1702   star_n_less <-- {hypreal,hypnat}_less
  1703   star_n_zero_num <-- {hypreal,hypnat,hcomplex}_zero_num
  1704   star_n_one_num <-- {hypreal,hypnat,hcomplex}_one_num
  1705   star_n_abs <-- hypreal_hrabs
  1706   star_n_divide <-- hcomplex_divide
  1707 
  1708   star_of_add <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_add
  1709   star_of_minus <-- {hypreal_of_real,hcomplex_of_complex}_minus
  1710   star_of_diff <-- hypreal_of_real_diff
  1711   star_of_mult <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_mult
  1712   star_of_one <-- {hypreal_of_real,hcomplex_of_complex}_one
  1713   star_of_zero <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_zero
  1714   star_of_le <-- {hypreal_of_real,hypnat_of_nat}_le_iff
  1715   star_of_less <-- {hypreal_of_real,hypnat_of_nat}_less_iff
  1716   star_of_eq <-- {hypreal_of_real,hypnat_of_nat,hcomplex_of_complex}_eq_iff
  1717   star_of_inverse <-- {hypreal_of_real,hcomplex_of_complex}_inverse
  1718   star_of_divide <-- {hypreal_of_real,hcomplex_of_complex}_divide
  1719   star_of_of_nat <-- {hypreal_of_real,hcomplex_of_complex}_of_nat
  1720   star_of_of_int <-- {hypreal_of_real,hcomplex_of_complex}_of_int
  1721   star_of_number_of <-- {hypreal,hcomplex}_number_of
  1722   star_of_number_less <-- number_of_less_hypreal_of_real_iff
  1723   star_of_number_le <-- number_of_le_hypreal_of_real_iff
  1724   star_of_eq_number <-- hypreal_of_real_eq_number_of_iff
  1725   star_of_less_number <-- hypreal_of_real_less_number_of_iff
  1726   star_of_le_number <-- hypreal_of_real_le_number_of_iff
  1727   star_of_power <-- hypreal_of_real_power
  1728   star_of_eq_0 <-- hcomplex_of_complex_zero_iff
  1729 
  1730 * Hyperreal: new method "transfer" that implements the transfer
  1731 principle of nonstandard analysis. With a subgoal that mentions
  1732 nonstandard types like "'a star", the command "apply transfer"
  1733 replaces it with an equivalent one that mentions only standard types.
  1734 To be successful, all free variables must have standard types; non-
  1735 standard variables must have explicit universal quantifiers.
  1736 
  1737 * Hyperreal: A theory of Taylor series.
  1738 
  1739 
  1740 *** HOLCF ***
  1741 
  1742 * Discontinued special version of 'constdefs' (which used to support
  1743 continuous functions) in favor of the general Pure one with full
  1744 type-inference.
  1745 
  1746 * New simplification procedure for solving continuity conditions; it
  1747 is much faster on terms with many nested lambda abstractions (cubic
  1748 instead of exponential time).
  1749 
  1750 * New syntax for domain package: selector names are now optional.
  1751 Parentheses should be omitted unless argument is lazy, for example:
  1752 
  1753   domain 'a stream = cons "'a" (lazy "'a stream")
  1754 
  1755 * New command 'fixrec' for defining recursive functions with pattern
  1756 matching; defining multiple functions with mutual recursion is also
  1757 supported.  Patterns may include the constants cpair, spair, up, sinl,
  1758 sinr, or any data constructor defined by the domain package. The given
  1759 equations are proven as rewrite rules. See HOLCF/ex/Fixrec_ex.thy for
  1760 syntax and examples.
  1761 
  1762 * New commands 'cpodef' and 'pcpodef' for defining predicate subtypes
  1763 of cpo and pcpo types. Syntax is exactly like the 'typedef' command,
  1764 but the proof obligation additionally includes an admissibility
  1765 requirement. The packages generate instances of class cpo or pcpo,
  1766 with continuity and strictness theorems for Rep and Abs.
  1767 
  1768 * HOLCF: Many theorems have been renamed according to a more standard naming
  1769 scheme (INCOMPATIBILITY):
  1770 
  1771   foo_inject:  "foo$x = foo$y ==> x = y"
  1772   foo_eq:      "(foo$x = foo$y) = (x = y)"
  1773   foo_less:    "(foo$x << foo$y) = (x << y)"
  1774   foo_strict:  "foo$UU = UU"
  1775   foo_defined: "... ==> foo$x ~= UU"
  1776   foo_defined_iff: "(foo$x = UU) = (x = UU)"
  1777 
  1778 
  1779 *** ZF ***
  1780 
  1781 * ZF/ex: theories Group and Ring provide examples in abstract algebra,
  1782 including the First Isomorphism Theorem (on quotienting by the kernel
  1783 of a homomorphism).
  1784 
  1785 * ZF/Simplifier: install second copy of type solver that actually
  1786 makes use of TC rules declared to Isar proof contexts (or locales);
  1787 the old version is still required for ML proof scripts.
  1788 
  1789 
  1790 *** Cube ***
  1791 
  1792 * Converted to Isar theory format; use locales instead of axiomatic
  1793 theories.
  1794 
  1795 
  1796 *** ML ***
  1797 
  1798 * Pure/library.ML: added ##>, ##>>, #>> -- higher-order counterparts
  1799 for ||>, ||>>, |>>,
  1800 
  1801 * Pure/library.ML no longer defines its own option datatype, but uses
  1802 that of the SML basis, which has constructors NONE and SOME instead of
  1803 None and Some, as well as exception Option.Option instead of OPTION.
  1804 The functions the, if_none, is_some, is_none have been adapted
  1805 accordingly, while Option.map replaces apsome.
  1806 
  1807 * Pure/library.ML: the exception LIST has been given up in favour of
  1808 the standard exceptions Empty and Subscript, as well as
  1809 Library.UnequalLengths.  Function like Library.hd and Library.tl are
  1810 superceded by the standard hd and tl functions etc.
  1811 
  1812 A number of basic list functions are no longer exported to the ML
  1813 toplevel, as they are variants of predefined functions.  The following
  1814 suggests how one can translate existing code:
  1815 
  1816     rev_append xs ys = List.revAppend (xs, ys)
  1817     nth_elem (i, xs) = List.nth (xs, i)
  1818     last_elem xs = List.last xs
  1819     flat xss = List.concat xss
  1820     seq fs = List.app fs
  1821     partition P xs = List.partition P xs
  1822     mapfilter f xs = List.mapPartial f xs
  1823 
  1824 * Pure/library.ML: several combinators for linear functional
  1825 transformations, notably reverse application and composition:
  1826 
  1827   x |> f                f #> g
  1828   (x, y) |-> f          f #-> g
  1829 
  1830 * Pure/library.ML: introduced/changed precedence of infix operators:
  1831 
  1832   infix 1 |> |-> ||> ||>> |>> |>>> #> #->;
  1833   infix 2 ?;
  1834   infix 3 o oo ooo oooo;
  1835   infix 4 ~~ upto downto;
  1836 
  1837 Maybe INCOMPATIBILITY when any of those is used in conjunction with other
  1838 infix operators.
  1839 
  1840 * Pure/library.ML: natural list combinators fold, fold_rev, and
  1841 fold_map support linear functional transformations and nesting.  For
  1842 example:
  1843 
  1844   fold f [x1, ..., xN] y =
  1845     y |> f x1 |> ... |> f xN
  1846 
  1847   (fold o fold) f [xs1, ..., xsN] y =
  1848     y |> fold f xs1 |> ... |> fold f xsN
  1849 
  1850   fold f [x1, ..., xN] =
  1851     f x1 #> ... #> f xN
  1852 
  1853   (fold o fold) f [xs1, ..., xsN] =
  1854     fold f xs1 #> ... #> fold f xsN
  1855 
  1856 * Pure/library.ML: the following selectors on type 'a option are
  1857 available:
  1858 
  1859   the:               'a option -> 'a  (*partial*)
  1860   these:             'a option -> 'a  where 'a = 'b list
  1861   the_default: 'a -> 'a option -> 'a
  1862   the_list:          'a option -> 'a list
  1863 
  1864 * Pure/General: structure AList (cf. Pure/General/alist.ML) provides
  1865 basic operations for association lists, following natural argument
  1866 order; moreover the explicit equality predicate passed here avoids
  1867 potentially expensive polymorphic runtime equality checks.
  1868 The old functions may be expressed as follows:
  1869 
  1870   assoc = uncurry (AList.lookup (op =))
  1871   assocs = these oo AList.lookup (op =)
  1872   overwrite = uncurry (AList.update (op =)) o swap
  1873 
  1874 * Pure/General: structure AList (cf. Pure/General/alist.ML) provides
  1875 
  1876   val make: ('a -> 'b) -> 'a list -> ('a * 'b) list
  1877   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
  1878 
  1879 replacing make_keylist and keyfilter (occassionally used)
  1880 Naive rewrites:
  1881 
  1882   make_keylist = AList.make
  1883   keyfilter = AList.find (op =)
  1884 
  1885 * eq_fst and eq_snd now take explicit equality parameter, thus
  1886   avoiding eqtypes. Naive rewrites:
  1887 
  1888     eq_fst = eq_fst (op =)
  1889     eq_snd = eq_snd (op =)
  1890 
  1891 * Removed deprecated apl and apr (rarely used).
  1892   Naive rewrites:
  1893 
  1894     apl (n, op) =>>= curry op n
  1895     apr (op, m) =>>= fn n => op (n, m)
  1896 
  1897 * Pure/General: structure OrdList (cf. Pure/General/ord_list.ML)
  1898 provides a reasonably efficient light-weight implementation of sets as
  1899 lists.
  1900 
  1901 * Pure/General: generic tables (cf. Pure/General/table.ML) provide a
  1902 few new operations; existing lookup and update are now curried to
  1903 follow natural argument order (for use with fold etc.);
  1904 INCOMPATIBILITY, use (uncurry Symtab.lookup) etc. as last resort.
  1905 
  1906 * Pure/General: output via the Isabelle channels of
  1907 writeln/warning/error etc. is now passed through Output.output, with a
  1908 hook for arbitrary transformations depending on the print_mode
  1909 (cf. Output.add_mode -- the first active mode that provides a output
  1910 function wins).  Already formatted output may be embedded into further
  1911 text via Output.raw; the result of Pretty.string_of/str_of and derived
  1912 functions (string_of_term/cterm/thm etc.) is already marked raw to
  1913 accommodate easy composition of diagnostic messages etc.  Programmers
  1914 rarely need to care about Output.output or Output.raw at all, with
  1915 some notable exceptions: Output.output is required when bypassing the
  1916 standard channels (writeln etc.), or in token translations to produce
  1917 properly formatted results; Output.raw is required when capturing
  1918 already output material that will eventually be presented to the user
  1919 a second time.  For the default print mode, both Output.output and
  1920 Output.raw have no effect.
  1921 
  1922 * Pure/General: Output.time_accumulator NAME creates an operator ('a
  1923 -> 'b) -> 'a -> 'b to measure runtime and count invocations; the
  1924 cumulative results are displayed at the end of a batch session.
  1925 
  1926 * Pure/General: File.sysify_path and File.quote_sysify path have been
  1927 replaced by File.platform_path and File.shell_path (with appropriate
  1928 hooks).  This provides a clean interface for unusual systems where the
  1929 internal and external process view of file names are different.
  1930 
  1931 * Pure: more efficient orders for basic syntactic entities: added
  1932 fast_string_ord, fast_indexname_ord, fast_term_ord; changed sort_ord
  1933 and typ_ord to use fast_string_ord and fast_indexname_ord (term_ord is
  1934 NOT affected); structures Symtab, Vartab, Typtab, Termtab use the fast
  1935 orders now -- potential INCOMPATIBILITY for code that depends on a
  1936 particular order for Symtab.keys, Symtab.dest, etc. (consider using
  1937 Library.sort_strings on result).
  1938 
  1939 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types,
  1940 fold_types traverse types/terms from left to right, observing natural
  1941 argument order.  Supercedes previous foldl_XXX versions, add_frees,
  1942 add_vars etc. have been adapted as well: INCOMPATIBILITY.
  1943 
  1944 * Pure: name spaces have been refined, with significant changes of the
  1945 internal interfaces -- INCOMPATIBILITY.  Renamed cond_extern(_table)
  1946 to extern(_table).  The plain name entry path is superceded by a
  1947 general 'naming' context, which also includes the 'policy' to produce
  1948 a fully qualified name and external accesses of a fully qualified
  1949 name; NameSpace.extend is superceded by context dependent
  1950 Sign.declare_name.  Several theory and proof context operations modify
  1951 the naming context.  Especially note Theory.restore_naming and
  1952 ProofContext.restore_naming to get back to a sane state; note that
  1953 Theory.add_path is no longer sufficient to recover from
  1954 Theory.absolute_path in particular.
  1955 
  1956 * Pure: new flags short_names (default false) and unique_names
  1957 (default true) for controlling output of qualified names.  If
  1958 short_names is set, names are printed unqualified.  If unique_names is
  1959 reset, the name prefix is reduced to the minimum required to achieve
  1960 the original result when interning again, even if there is an overlap
  1961 with earlier declarations.
  1962 
  1963 * Pure/TheoryDataFun: change of the argument structure; 'prep_ext' is
  1964 now 'extend', and 'merge' gets an additional Pretty.pp argument
  1965 (useful for printing error messages).  INCOMPATIBILITY.
  1966 
  1967 * Pure: major reorganization of the theory context.  Type Sign.sg and
  1968 Theory.theory are now identified, referring to the universal
  1969 Context.theory (see Pure/context.ML).  Actual signature and theory
  1970 content is managed as theory data.  The old code and interfaces were
  1971 spread over many files and structures; the new arrangement introduces
  1972 considerable INCOMPATIBILITY to gain more clarity:
  1973 
  1974   Context -- theory management operations (name, identity, inclusion,
  1975     parents, ancestors, merge, etc.), plus generic theory data;
  1976 
  1977   Sign -- logical signature and syntax operations (declaring consts,
  1978     types, etc.), plus certify/read for common entities;
  1979 
  1980   Theory -- logical theory operations (stating axioms, definitions,
  1981     oracles), plus a copy of logical signature operations (consts,
  1982     types, etc.); also a few basic management operations (Theory.copy,
  1983     Theory.merge, etc.)
  1984 
  1985 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm
  1986 etc.) as well as the sign field in Thm.rep_thm etc. have been retained
  1987 for convenience -- they merely return the theory.
  1988 
  1989 * Pure: type Type.tsig is superceded by theory in most interfaces.
  1990 
  1991 * Pure: the Isar proof context type is already defined early in Pure
  1992 as Context.proof (note that ProofContext.context and Proof.context are
  1993 aliases, where the latter is the preferred name).  This enables other
  1994 Isabelle components to refer to that type even before Isar is present.
  1995 
  1996 * Pure/sign/theory: discontinued named name spaces (i.e. classK,
  1997 typeK, constK, axiomK, oracleK), but provide explicit operations for
  1998 any of these kinds.  For example, Sign.intern typeK is now
  1999 Sign.intern_type, Theory.hide_space Sign.typeK is now
  2000 Theory.hide_types.  Also note that former
  2001 Theory.hide_classes/types/consts are now
  2002 Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions
  2003 internalize their arguments!  INCOMPATIBILITY.
  2004 
  2005 * Pure: get_thm interface (of PureThy and ProofContext) expects
  2006 datatype thmref (with constructors Name and NameSelection) instead of
  2007 plain string -- INCOMPATIBILITY;
  2008 
  2009 * Pure: cases produced by proof methods specify options, where NONE
  2010 means to remove case bindings -- INCOMPATIBILITY in
  2011 (RAW_)METHOD_CASES.
  2012 
  2013 * Pure: the following operations retrieve axioms or theorems from a
  2014 theory node or theory hierarchy, respectively:
  2015 
  2016   Theory.axioms_of: theory -> (string * term) list
  2017   Theory.all_axioms_of: theory -> (string * term) list
  2018   PureThy.thms_of: theory -> (string * thm) list
  2019   PureThy.all_thms_of: theory -> (string * thm) list
  2020 
  2021 * Pure: print_tac now outputs the goal through the trace channel.
  2022 
  2023 * Isar toplevel: improved diagnostics, mostly for Poly/ML only.
  2024 Reference Toplevel.debug (default false) controls detailed printing
  2025 and tracing of low-level exceptions; Toplevel.profiling (default 0)
  2026 controls execution profiling -- set to 1 for time and 2 for space
  2027 (both increase the runtime).
  2028 
  2029 * Isar session: The initial use of ROOT.ML is now always timed,
  2030 i.e. the log will show the actual process times, in contrast to the
  2031 elapsed wall-clock time that the outer shell wrapper produces.
  2032 
  2033 * Simplifier: improved handling of bound variables (nameless
  2034 representation, avoid allocating new strings).  Simprocs that invoke
  2035 the Simplifier recursively should use Simplifier.inherit_bounds to
  2036 avoid local name clashes.  Failure to do so produces warnings
  2037 "Simplifier: renamed bound variable ..."; set Simplifier.debug_bounds
  2038 for further details.
  2039 
  2040 * ML functions legacy_bindings and use_legacy_bindings produce ML fact
  2041 bindings for all theorems stored within a given theory; this may help
  2042 in porting non-Isar theories to Isar ones, while keeping ML proof
  2043 scripts for the time being.
  2044 
  2045 * ML operator HTML.with_charset specifies the charset begin used for
  2046 generated HTML files.  For example:
  2047 
  2048   HTML.with_charset "utf-8" use_thy "Hebrew";
  2049   HTML.with_charset "utf-8" use_thy "Chinese";
  2050 
  2051 
  2052 *** System ***
  2053 
  2054 * Allow symlinks to all proper Isabelle executables (Isabelle,
  2055 isabelle, isatool etc.).
  2056 
  2057 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for
  2058 isatool doc, isatool mkdir, display_drafts etc.).
  2059 
  2060 * isatool usedir: option -f allows specification of the ML file to be
  2061 used by Isabelle; default is ROOT.ML.
  2062 
  2063 * New isatool version outputs the version identifier of the Isabelle
  2064 distribution being used.
  2065 
  2066 * HOL: new isatool dimacs2hol converts files in DIMACS CNF format
  2067 (containing Boolean satisfiability problems) into Isabelle/HOL
  2068 theories.
  2069 
  2070 
  2071 
  2072 New in Isabelle2004 (April 2004)
  2073 --------------------------------
  2074 
  2075 *** General ***
  2076 
  2077 * Provers/order.ML:  new efficient reasoner for partial and linear orders.
  2078   Replaces linorder.ML.
  2079 
  2080 * Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic
  2081   (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler
  2082   (\<a>...\<z>), are now considered normal letters, and can therefore
  2083   be used anywhere where an ASCII letter (a...zA...Z) has until
  2084   now. COMPATIBILITY: This obviously changes the parsing of some
  2085   terms, especially where a symbol has been used as a binder, say
  2086   '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
  2087   as an identifier.  Fix it by inserting a space around former
  2088   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
  2089   existing theory and ML files.
  2090 
  2091 * Pure: Macintosh and Windows line-breaks are now allowed in theory files.
  2092 
  2093 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now
  2094   allowed in identifiers. Similar to Greek letters \<^isub> is now considered
  2095   a normal (but invisible) letter. For multiple letter subscripts repeat
  2096   \<^isub> like this: x\<^isub>1\<^isub>2.
  2097 
  2098 * Pure: There are now sub-/superscripts that can span more than one
  2099   character. Text between \<^bsub> and \<^esub> is set in subscript in
  2100   ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
  2101   superscript. The new control characters are not identifier parts.
  2102 
  2103 * Pure: Control-symbols of the form \<^raw:...> will literally print the
  2104   content of "..." to the latex file instead of \isacntrl... . The "..."
  2105   may consist of any printable characters excluding the end bracket >.
  2106 
  2107 * Pure: Using new Isar command "finalconsts" (or the ML functions
  2108   Theory.add_finals or Theory.add_finals_i) it is now possible to
  2109   declare constants "final", which prevents their being given a definition
  2110   later.  It is useful for constants whose behaviour is fixed axiomatically
  2111   rather than definitionally, such as the meta-logic connectives.
  2112 
  2113 * Pure: 'instance' now handles general arities with general sorts
  2114   (i.e. intersections of classes),
  2115 
  2116 * Presentation: generated HTML now uses a CSS style sheet to make layout
  2117   (somewhat) independent of content. It is copied from lib/html/isabelle.css.
  2118   It can be changed to alter the colors/layout of generated pages.
  2119 
  2120 
  2121 *** Isar ***
  2122 
  2123 * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
  2124   cut_tac, subgoal_tac and thin_tac:
  2125   - Now understand static (Isar) contexts.  As a consequence, users of Isar
  2126     locales are no longer forced to write Isar proof scripts.
  2127     For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
  2128     emulations.
  2129   - INCOMPATIBILITY: names of variables to be instantiated may no
  2130     longer be enclosed in quotes.  Instead, precede variable name with `?'.
  2131     This is consistent with the instantiation attribute "where".
  2132 
  2133 * Attributes "where" and "of":
  2134   - Now take type variables of instantiated theorem into account when reading
  2135     the instantiation string.  This fixes a bug that caused instantiated
  2136     theorems to have too special types in some circumstances.
  2137   - "where" permits explicit instantiations of type variables.
  2138 
  2139 * Calculation commands "moreover" and "also" no longer interfere with
  2140   current facts ("this"), admitting arbitrary combinations with "then"
  2141   and derived forms.
  2142 
  2143 * Locales:
  2144   - Goal statements involving the context element "includes" no longer
  2145     generate theorems with internal delta predicates (those ending on
  2146     "_axioms") in the premise.
  2147     Resolve particular premise with <locale>.intro to obtain old form.
  2148   - Fixed bug in type inference ("unify_frozen") that prevented mix of target
  2149     specification and "includes" elements in goal statement.
  2150   - Rule sets <locale>.intro and <locale>.axioms no longer declared as
  2151     [intro?] and [elim?] (respectively) by default.
  2152   - Experimental command for instantiation of locales in proof contexts:
  2153         instantiate <label>[<attrs>]: <loc>
  2154     Instantiates locale <loc> and adds all its theorems to the current context
  2155     taking into account their attributes.  Label and attrs are optional
  2156     modifiers, like in theorem declarations.  If present, names of
  2157     instantiated theorems are qualified with <label>, and the attributes
  2158     <attrs> are applied after any attributes these theorems might have already.
  2159       If the locale has assumptions, a chained fact of the form
  2160     "<loc> t1 ... tn" is expected from which instantiations of the parameters
  2161     are derived.  The command does not support old-style locales declared
  2162     with "locale (open)".
  2163       A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
  2164 
  2165 * HOL: Tactic emulation methods induct_tac and case_tac understand static
  2166   (Isar) contexts.
  2167 
  2168 
  2169 *** HOL ***
  2170 
  2171 * Proof import: new image HOL4 contains the imported library from
  2172   the HOL4 system with about 2500 theorems. It is imported by
  2173   replaying proof terms produced by HOL4 in Isabelle. The HOL4 image
  2174   can be used like any other Isabelle image.  See
  2175   HOL/Import/HOL/README for more information.
  2176 
  2177 * Simplifier:
  2178   - Much improved handling of linear and partial orders.
  2179     Reasoners for linear and partial orders are set up for type classes
  2180     "linorder" and "order" respectively, and are added to the default simpset
  2181     as solvers.  This means that the simplifier can build transitivity chains
  2182     to solve goals from the assumptions.
  2183   - INCOMPATIBILITY: old proofs break occasionally.  Typically, applications
  2184     of blast or auto after simplification become unnecessary because the goal
  2185     is solved by simplification already.
  2186 
  2187 * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws,
  2188     all proved in axiomatic type classes for semirings, rings and fields.
  2189 
  2190 * Numerics:
  2191   - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are
  2192     now formalized using the Ring_and_Field theory mentioned above.
  2193   - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently
  2194     than before, because now they are set up once in a generic manner.
  2195   - INCOMPATIBILITY: many type-specific arithmetic laws have gone.
  2196     Look for the general versions in Ring_and_Field (and Power if they concern
  2197     exponentiation).
  2198 
  2199 * Type "rat" of the rational numbers is now available in HOL-Complex.
  2200 
  2201 * Records:
  2202   - Record types are now by default printed with their type abbreviation
  2203     instead of the list of all field types. This can be configured via
  2204     the reference "print_record_type_abbr".
  2205   - Simproc "record_upd_simproc" for simplification of multiple updates added
  2206     (not enabled by default).
  2207   - Simproc "record_ex_sel_eq_simproc" to simplify EX x. sel r = x resp.
  2208     EX x. x = sel r to True (not enabled by default).
  2209   - Tactic "record_split_simp_tac" to split and simplify records added.
  2210 
  2211 * 'specification' command added, allowing for definition by
  2212   specification.  There is also an 'ax_specification' command that
  2213   introduces the new constants axiomatically.
  2214 
  2215 * arith(_tac) is now able to generate counterexamples for reals as well.
  2216 
  2217 * HOL-Algebra: new locale "ring" for non-commutative rings.
  2218 
  2219 * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
  2220   definitions, thanks to Sava Krsti\'{c} and John Matthews.
  2221 
  2222 * HOL-Matrix: a first theory for matrices in HOL with an application of
  2223   matrix theory to linear programming.
  2224 
  2225 * Unions and Intersections:
  2226   The latex output syntax of UN and INT has been changed
  2227   from "\Union x \in A. B" to "\Union_{x \in A} B"
  2228   i.e. the index formulae has become a subscript.
  2229   Similarly for "\Union x. B", and for \Inter instead of \Union.
  2230 
  2231 * Unions and Intersections over Intervals:
  2232   There is new short syntax "UN i<=n. A" for "UN i:{0..n}. A". There is
  2233   also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A"
  2234   like in normal math, and corresponding versions for < and for intersection.
  2235 
  2236 * HOL/List: Ordering "lexico" is renamed "lenlex" and the standard
  2237   lexicographic dictonary ordering has been added as "lexord".
  2238 
  2239 * ML: the legacy theory structures Int and List have been removed. They had
  2240   conflicted with ML Basis Library structures having the same names.
  2241 
  2242 * 'refute' command added to search for (finite) countermodels.  Only works
  2243   for a fragment of HOL.  The installation of an external SAT solver is
  2244   highly recommended.  See "HOL/Refute.thy" for details.
  2245 
  2246 * 'quickcheck' command: Allows to find counterexamples by evaluating
  2247   formulae under an assignment of free variables to random values.
  2248   In contrast to 'refute', it can deal with inductive datatypes,
  2249   but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy"
  2250   for examples.
  2251 
  2252 
  2253 *** HOLCF ***
  2254 
  2255 * Streams now come with concatenation and are part of the HOLCF image
  2256 
  2257 
  2258 
  2259 New in Isabelle2003 (May 2003)
  2260 ------------------------------
  2261 
  2262 *** General ***
  2263 
  2264 * Provers/simplifier:
  2265 
  2266   - Completely reimplemented method simp (ML: Asm_full_simp_tac):
  2267     Assumptions are now subject to complete mutual simplification,
  2268     not just from left to right. The simplifier now preserves
  2269     the order of assumptions.
  2270 
  2271     Potential INCOMPATIBILITY:
  2272 
  2273     -- simp sometimes diverges where the old version did
  2274        not, e.g. invoking simp on the goal
  2275 
  2276         [| P (f x); y = x; f x = f y |] ==> Q
  2277 
  2278        now gives rise to the infinite reduction sequence
  2279 
  2280         P(f x) --(f x = f y)--> P(f y) --(y = x)--> P(f x) --(f x = f y)--> ...
  2281 
  2282        Using "simp (asm_lr)" (ML: Asm_lr_simp_tac) instead often solves this
  2283        kind of problem.
  2284 
  2285     -- Tactics combining classical reasoner and simplification (such as auto)
  2286        are also affected by this change, because many of them rely on
  2287        simp. They may sometimes diverge as well or yield a different numbers
  2288        of subgoals. Try to use e.g. force, fastsimp, or safe instead of auto
  2289        in case of problems. Sometimes subsequent calls to the classical
  2290        reasoner will fail because a preceeding call to the simplifier too
  2291        eagerly simplified the goal, e.g. deleted redundant premises.
  2292 
  2293   - The simplifier trace now shows the names of the applied rewrite rules
  2294 
  2295   - You can limit the number of recursive invocations of the simplifier
  2296     during conditional rewriting (where the simplifie tries to solve the
  2297     conditions before applying the rewrite rule):
  2298     ML "simp_depth_limit := n"
  2299     where n is an integer. Thus you can force termination where previously
  2300     the simplifier would diverge.
  2301 
  2302   - Accepts free variables as head terms in congruence rules.  Useful in Isar.
  2303 
  2304   - No longer aborts on failed congruence proof.  Instead, the
  2305     congruence is ignored.
  2306 
  2307 * Pure: New generic framework for extracting programs from constructive
  2308   proofs. See HOL/Extraction.thy for an example instantiation, as well
  2309   as HOL/Extraction for some case studies.
  2310 
  2311 * Pure: The main goal of the proof state is no longer shown by default, only
  2312 the subgoals. This behaviour is controlled by a new flag.
  2313    PG menu: Isabelle/Isar -> Settings -> Show Main Goal
  2314 (ML: Proof.show_main_goal).
  2315 
  2316 * Pure: You can find all matching introduction rules for subgoal 1, i.e. all
  2317 rules whose conclusion matches subgoal 1:
  2318       PG menu: Isabelle/Isar -> Show me -> matching rules
  2319 The rules are ordered by how closely they match the subgoal.
  2320 In particular, rules that solve a subgoal outright are displayed first
  2321 (or rather last, the way they are printed).
  2322 (ML: ProofGeneral.print_intros())
  2323 
  2324 * Pure: New flag trace_unify_fail causes unification to print
  2325 diagnostic information (PG: in trace buffer) when it fails. This is
  2326 useful for figuring out why single step proofs like rule, erule or
  2327 assumption failed.
  2328 
  2329 * Pure: Locale specifications now produce predicate definitions
  2330 according to the body of text (covering assumptions modulo local
  2331 definitions); predicate "loc_axioms" covers newly introduced text,
  2332 while "loc" is cumulative wrt. all included locale expressions; the
  2333 latter view is presented only on export into the global theory
  2334 context; potential INCOMPATIBILITY, use "(open)" option to fall back
  2335 on the old view without predicates;
  2336 
  2337 * Pure: predefined locales "var" and "struct" are useful for sharing
  2338 parameters (as in CASL, for example); just specify something like
  2339 ``var x + var y + struct M'' as import;
  2340 
  2341 * Pure: improved thms_containing: proper indexing of facts instead of
  2342 raw theorems; check validity of results wrt. current name space;
  2343 include local facts of proof configuration (also covers active
  2344 locales), cover fixed variables in index; may use "_" in term
  2345 specification; an optional limit for the number of printed facts may
  2346 be given (the default is 40);
  2347 
  2348 * Pure: disallow duplicate fact bindings within new-style theory files
  2349 (batch-mode only);
  2350 
  2351 * Provers: improved induct method: assumptions introduced by case
  2352 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from
  2353 the goal statement); "foo" still refers to all facts collectively;
  2354 
  2355 * Provers: the function blast.overloaded has been removed: all constants
  2356 are regarded as potentially overloaded, which improves robustness in exchange
  2357 for slight decrease in efficiency;
  2358 
  2359 * Provers/linorder: New generic prover for transitivity reasoning over
  2360 linear orders.  Note: this prover is not efficient!
  2361 
  2362 * Isar: preview of problems to finish 'show' now produce an error
  2363 rather than just a warning (in interactive mode);
  2364 
  2365 
  2366 *** HOL ***
  2367 
  2368 * arith(_tac)
  2369 
  2370  - Produces a counter example if it cannot prove a goal.
  2371    Note that the counter example may be spurious if the goal is not a formula
  2372    of quantifier-free linear arithmetic.
  2373    In ProofGeneral the counter example appears in the trace buffer.
  2374 
  2375  - Knows about div k and mod k where k is a numeral of type nat or int.
  2376 
  2377  - Calls full Presburger arithmetic (by Amine Chaieb) if quantifier-free
  2378    linear arithmetic fails. This takes account of quantifiers and divisibility.
  2379    Presburger arithmetic can also be called explicitly via presburger(_tac).
  2380 
  2381 * simp's arithmetic capabilities have been enhanced a bit: it now
  2382 takes ~= in premises into account (by performing a case split);
  2383 
  2384 * simp reduces "m*(n div m) + n mod m" to n, even if the two summands
  2385 are distributed over a sum of terms;
  2386 
  2387 * New tactic "trans_tac" and method "trans" instantiate
  2388 Provers/linorder.ML for axclasses "order" and "linorder" (predicates
  2389 "<=", "<" and "=").
  2390 
  2391 * function INCOMPATIBILITIES: Pi-sets have been redefined and moved from main
  2392 HOL to Library/FuncSet; constant "Fun.op o" is now called "Fun.comp";
  2393 
  2394 * 'typedef' command has new option "open" to suppress the set
  2395 definition;
  2396 
  2397 * functions Min and Max on finite sets have been introduced (theory
  2398 Finite_Set);
  2399 
  2400 * attribute [symmetric] now works for relations as well; it turns
  2401 (x,y) : R^-1 into (y,x) : R, and vice versa;
  2402 
  2403 * induct over a !!-quantified statement (say !!x1..xn):
  2404   each "case" automatically performs "fix x1 .. xn" with exactly those names.
  2405 
  2406 * Map: `empty' is no longer a constant but a syntactic abbreviation for
  2407 %x. None. Warning: empty_def now refers to the previously hidden definition
  2408 of the empty set.
  2409 
  2410 * Algebra: formalization of classical algebra.  Intended as base for
  2411 any algebraic development in Isabelle.  Currently covers group theory
  2412 (up to Sylow's theorem) and ring theory (Universal Property of
  2413 Univariate Polynomials).  Contributions welcome;
  2414 
  2415 * GroupTheory: deleted, since its material has been moved to Algebra;
  2416 
  2417 * Complex: new directory of the complex numbers with numeric constants,
  2418 nonstandard complex numbers, and some complex analysis, standard and
  2419 nonstandard (Jacques Fleuriot);
  2420 
  2421 * HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal;
  2422 
  2423 * Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques
  2424 Fleuriot);
  2425 
  2426 * Real/HahnBanach: updated and adapted to locales;
  2427 
  2428 * NumberTheory: added Gauss's law of quadratic reciprocity (by Avigad,
  2429 Gray and Kramer);
  2430 
  2431 * UNITY: added the Meier-Sanders theory of progress sets;
  2432 
  2433 * MicroJava: bytecode verifier and lightweight bytecode verifier
  2434 as abstract algorithms, instantiated to the JVM;
  2435 
  2436 * Bali: Java source language formalization. Type system, operational
  2437 semantics, axiomatic semantics. Supported language features:
  2438 classes, interfaces, objects,virtual methods, static methods,
  2439 static/instance fields, arrays, access modifiers, definite
  2440 assignment, exceptions.
  2441 
  2442 
  2443 *** ZF ***
  2444 
  2445 * ZF/Constructible: consistency proof for AC (Gdel's constructible
  2446 universe, etc.);
  2447 
  2448 * Main ZF: virtually all theories converted to new-style format;
  2449 
  2450 
  2451 *** ML ***
  2452 
  2453 * Pure: Tactic.prove provides sane interface for internal proofs;
  2454 omits the infamous "standard" operation, so this is more appropriate
  2455 than prove_goalw_cterm in many situations (e.g. in simprocs);
  2456 
  2457 * Pure: improved error reporting of simprocs;
  2458 
  2459 * Provers: Simplifier.simproc(_i) provides sane interface for setting
  2460 up simprocs;
  2461 
  2462 
  2463 *** Document preparation ***
  2464 
  2465 * uses \par instead of \\ for line breaks in theory text. This may
  2466 shift some page breaks in large documents. To get the old behaviour
  2467 use \renewcommand{\isanewline}{\mbox{}\\\mbox{}} in root.tex.
  2468 
  2469 * minimized dependencies of isabelle.sty and isabellesym.sty on
  2470 other packages
  2471 
  2472 * \<euro> now needs package babel/greek instead of marvosym (which
  2473 broke \Rightarrow)
  2474 
  2475 * normal size for \<zero>...\<nine> (uses \mathbf instead of
  2476 textcomp package)
  2477 
  2478 
  2479 
  2480 New in Isabelle2002 (March 2002)
  2481 --------------------------------
  2482 
  2483 *** Document preparation ***
  2484 
  2485 * greatly simplified document preparation setup, including more
  2486 graceful interpretation of isatool usedir -i/-d/-D options, and more
  2487 instructive isatool mkdir; users should basically be able to get
  2488 started with "isatool mkdir HOL Test && isatool make"; alternatively,
  2489 users may run a separate document processing stage manually like this:
  2490 "isatool usedir -D output HOL Test && isatool document Test/output";
  2491 
  2492 * theory dependency graph may now be incorporated into documents;
  2493 isatool usedir -g true will produce session_graph.eps/.pdf for use
  2494 with \includegraphics of LaTeX;
  2495 
  2496 * proper spacing of consecutive markup elements, especially text
  2497 blocks after section headings;
  2498 
  2499 * support bold style (for single symbols only), input syntax is like
  2500 this: "\<^bold>\<alpha>" or "\<^bold>A";
  2501 
  2502 * \<bullet> is now output as bold \cdot by default, which looks much
  2503 better in printed text;
  2504 
  2505 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>;
  2506 note that these symbols are currently unavailable in Proof General /
  2507 X-Symbol; new symbols \<zero>, \<one>, ..., \<nine>, and \<euro>;
  2508 
  2509 * isatool latex no longer depends on changed TEXINPUTS, instead
  2510 isatool document copies the Isabelle style files to the target
  2511 location;
  2512 
  2513 
  2514 *** Isar ***
  2515 
  2516 * Pure/Provers: improved proof by cases and induction;
  2517   - 'case' command admits impromptu naming of parameters (such as
  2518     "case (Suc n)");
  2519   - 'induct' method divinates rule instantiation from the inductive
  2520     claim; no longer requires excessive ?P bindings for proper
  2521     instantiation of cases;
  2522   - 'induct' method properly enumerates all possibilities of set/type
  2523     rules; as a consequence facts may be also passed through *type*
  2524     rules without further ado;
  2525   - 'induct' method now derives symbolic cases from the *rulified*
  2526     rule (before it used to rulify cases stemming from the internal
  2527     atomized version); this means that the context of a non-atomic
  2528     statement becomes is included in the hypothesis, avoiding the
  2529     slightly cumbersome show "PROP ?case" form;
  2530   - 'induct' may now use elim-style induction rules without chaining
  2531     facts, using ``missing'' premises from the goal state; this allows
  2532     rules stemming from inductive sets to be applied in unstructured
  2533     scripts, while still benefitting from proper handling of non-atomic
  2534     statements; NB: major inductive premises need to be put first, all
  2535     the rest of the goal is passed through the induction;
  2536   - 'induct' proper support for mutual induction involving non-atomic
  2537     rule statements (uses the new concept of simultaneous goals, see
  2538     below);
  2539   - append all possible rule selections, but only use the first
  2540     success (no backtracking);
  2541   - removed obsolete "(simplified)" and "(stripped)" options of methods;
  2542   - undeclared rule case names default to numbers 1, 2, 3, ...;
  2543   - added 'print_induct_rules' (covered by help item in recent Proof
  2544     General versions);
  2545   - moved induct/cases attributes to Pure, methods to Provers;
  2546   - generic method setup instantiated for FOL and HOL;
  2547 
  2548 * Pure: support multiple simultaneous goal statements, for example
  2549 "have a: A and b: B" (same for 'theorem' etc.); being a pure
  2550 meta-level mechanism, this acts as if several individual goals had
  2551 been stated separately; in particular common proof methods need to be
  2552 repeated in order to cover all claims; note that a single elimination
  2553 step is *not* sufficient to establish the two conjunctions, so this
  2554 fails:
  2555 
  2556   assume "A & B" then have A and B ..   (*".." fails*)
  2557 
  2558 better use "obtain" in situations as above; alternative refer to
  2559 multi-step methods like 'auto', 'simp_all', 'blast+' etc.;
  2560 
  2561 * Pure: proper integration with ``locales''; unlike the original
  2562 version by Florian Kammller, Isar locales package high-level proof
  2563 contexts rather than raw logical ones (e.g. we admit to include
  2564 attributes everywhere); operations on locales include merge and
  2565 rename; support for implicit arguments (``structures''); simultaneous
  2566 type-inference over imports and text; see also HOL/ex/Locales.thy for
  2567 some examples;
  2568 
  2569 * Pure: the following commands have been ``localized'', supporting a
  2570 target locale specification "(in name)": 'lemma', 'theorem',
  2571 'corollary', 'lemmas', 'theorems', 'declare'; the results will be
  2572 stored both within the locale and at the theory level (exported and
  2573 qualified by the locale name);
  2574 
  2575 * Pure: theory goals may now be specified in ``long'' form, with
  2576 ad-hoc contexts consisting of arbitrary locale elements. for example
  2577 ``lemma foo: fixes x assumes "A x" shows "B x"'' (local syntax and
  2578 definitions may be given, too); the result is a meta-level rule with
  2579 the context elements being discharged in the obvious way;
  2580 
  2581 * Pure: new proof command 'using' allows to augment currently used
  2582 facts after a goal statement ('using' is syntactically analogous to
  2583 'apply', but acts on the goal's facts only); this allows chained facts
  2584 to be separated into parts given before and after a claim, as in
  2585 ``from a and b have C using d and e <proof>'';
  2586 
  2587 * Pure: renamed "antecedent" case to "rule_context";
  2588 
  2589 * Pure: new 'judgment' command records explicit information about the
  2590 object-logic embedding (used by several tools internally); no longer
  2591 use hard-wired "Trueprop";
  2592 
  2593 * Pure: added 'corollary' command;
  2594 
  2595 * Pure: fixed 'token_translation' command;
  2596 
  2597 * Pure: removed obsolete 'exported' attribute;
  2598 
  2599 * Pure: dummy pattern "_" in is/let is now automatically lifted over
  2600 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x")
  2601 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");
  2602 
  2603 * Pure: method 'atomize' presents local goal premises as object-level
  2604 statements (atomic meta-level propositions); setup controlled via
  2605 rewrite rules declarations of 'atomize' attribute; example
  2606 application: 'induct' method with proper rule statements in improper
  2607 proof *scripts*;
  2608 
  2609 * Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.)
  2610 now consider the syntactic context of assumptions, giving a better
  2611 chance to get type-inference of the arguments right (this is
  2612 especially important for locales);
  2613 
  2614 * Pure: "sorry" no longer requires quick_and_dirty in interactive
  2615 mode;
  2616 
  2617 * Pure/obtain: the formal conclusion "thesis", being marked as
  2618 ``internal'', may no longer be reference directly in the text;
  2619 potential INCOMPATIBILITY, may need to use "?thesis" in rare
  2620 situations;
  2621 
  2622 * Pure: generic 'sym' attribute which declares a rule both as pure
  2623 'elim?' and for the 'symmetric' operation;
  2624 
  2625 * Pure: marginal comments ``--'' may now occur just anywhere in the
  2626 text; the fixed correlation with particular command syntax has been
  2627 discontinued;
  2628 
  2629 * Pure: new method 'rules' is particularly well-suited for proof
  2630 search in intuitionistic logic; a bit slower than 'blast' or 'fast',
  2631 but often produces more compact proof terms with less detours;
  2632 
  2633 * Pure/Provers/classical: simplified integration with pure rule
  2634 attributes and methods; the classical "intro?/elim?/dest?"
  2635 declarations coincide with the pure ones; the "rule" method no longer
  2636 includes classically swapped intros; "intro" and "elim" methods no
  2637 longer pick rules from the context; also got rid of ML declarations
  2638 AddXIs/AddXEs/AddXDs; all of this has some potential for
  2639 INCOMPATIBILITY;
  2640 
  2641 * Provers/classical: attribute 'swapped' produces classical inversions
  2642 of introduction rules;
  2643 
  2644 * Provers/simplifier: 'simplified' attribute may refer to explicit
  2645 rules instead of full simplifier context; 'iff' attribute handles
  2646 conditional rules;
  2647 
  2648 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
  2649 
  2650 * HOL: 'recdef' now fails on unfinished automated proofs, use
  2651 "(permissive)" option to recover old behavior;
  2652 
  2653 * HOL: 'inductive' no longer features separate (collective) attributes
  2654 for 'intros' (was found too confusing);
  2655 
  2656 * HOL: properly declared induction rules less_induct and
  2657 wf_induct_rule;
  2658 
  2659 
  2660 *** HOL ***
  2661 
  2662 * HOL: moved over to sane numeral syntax; the new policy is as
  2663 follows:
  2664 
  2665   - 0 and 1 are polymorphic constants, which are defined on any
  2666   numeric type (nat, int, real etc.);
  2667 
  2668   - 2, 3, 4, ... and -1, -2, -3, ... are polymorphic numerals, based
  2669   binary representation internally;
  2670 
  2671   - type nat has special constructor Suc, and generally prefers Suc 0
  2672   over 1::nat and Suc (Suc 0) over 2::nat;
  2673 
  2674 This change may cause significant problems of INCOMPATIBILITY; here
  2675 are some hints on converting existing sources:
  2676 
  2677   - due to the new "num" token, "-0" and "-1" etc. are now atomic
  2678   entities, so expressions involving "-" (unary or binary minus) need
  2679   to be spaced properly;
  2680 
  2681   - existing occurrences of "1" may need to be constraint "1::nat" or
  2682   even replaced by Suc 0; similar for old "2";
  2683 
  2684   - replace "#nnn" by "nnn", and "#-nnn" by "-nnn";
  2685 
  2686   - remove all special provisions on numerals in proofs;
  2687 
  2688 * HOL: simp rules nat_number expand numerals on nat to Suc/0
  2689 representation (depends on bin_arith_simps in the default context);
  2690 
  2691 * HOL: symbolic syntax for x^2 (numeral 2);
  2692 
  2693 * HOL: the class of all HOL types is now called "type" rather than
  2694 "term"; INCOMPATIBILITY, need to adapt references to this type class
  2695 in axclass/classes, instance/arities, and (usually rare) occurrences
  2696 in typings (of consts etc.); internally the class is called
  2697 "HOL.type", ML programs should refer to HOLogic.typeS;
  2698 
  2699 * HOL/record package improvements:
  2700   - new derived operations "fields" to build a partial record section,
  2701     "extend" to promote a fixed record to a record scheme, and
  2702     "truncate" for the reverse; cf. theorems "xxx.defs", which are *not*
  2703     declared as simp by default;
  2704   - shared operations ("more", "fields", etc.) now need to be always
  2705     qualified) --- potential INCOMPATIBILITY;
  2706   - removed "make_scheme" operations (use "make" with "extend") --
  2707     INCOMPATIBILITY;
  2708   - removed "more" class (simply use "term") -- INCOMPATIBILITY;
  2709   - provides cases/induct rules for use with corresponding Isar
  2710     methods (for concrete records, record schemes, concrete more
  2711     parts, and schematic more parts -- in that order);
  2712   - internal definitions directly based on a light-weight abstract
  2713     theory of product types over typedef rather than datatype;
  2714 
  2715 * HOL: generic code generator for generating executable ML code from
  2716 specifications; specific support for HOL constructs such as inductive
  2717 datatypes and sets, as well as recursive functions; can be invoked
  2718 via 'generate_code' theory section;
  2719 
  2720 * HOL: canonical cases/induct rules for n-tuples (n = 3..7);
  2721 
  2722 * HOL: consolidated and renamed several theories.  In particular:
  2723         Ord.thy has been absorbed into HOL.thy
  2724         String.thy has been absorbed into List.thy
  2725 
  2726 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A"
  2727 (beware of argument permutation!);
  2728 
  2729 * HOL: linorder_less_split superseded by linorder_cases;
  2730 
  2731 * HOL/List: "nodups" renamed to "distinct";
  2732 
  2733 * HOL: added "The" definite description operator; move Hilbert's "Eps"
  2734 to peripheral theory "Hilbert_Choice"; some INCOMPATIBILITIES:
  2735   - Ex_def has changed, now need to use some_eq_ex
  2736 
  2737 * HOL: made split_all_tac safe; EXISTING PROOFS MAY FAIL OR LOOP, so
  2738 in this (rare) case use:
  2739 
  2740   delSWrapper "split_all_tac"
  2741   addSbefore ("unsafe_split_all_tac", unsafe_split_all_tac)
  2742 
  2743 * HOL: added safe wrapper "split_conv_tac" to claset; EXISTING PROOFS
  2744 MAY FAIL;
  2745 
  2746 * HOL: introduced f^n = f o ... o f; warning: due to the limits of
  2747 Isabelle's type classes, ^ on functions and relations has too general
  2748 a domain, namely ('a * 'b) set and 'a => 'b; this means that it may be
  2749 necessary to attach explicit type constraints;
  2750 
  2751 * HOL/Relation: the prefix name of the infix "O" has been changed from
  2752 "comp" to "rel_comp"; INCOMPATIBILITY: a few theorems have been
  2753 renamed accordingly (eg "compI" -> "rel_compI").
  2754 
  2755 * HOL: syntax translations now work properly with numerals and records
  2756 expressions;
  2757 
  2758 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead
  2759 of "lam" -- INCOMPATIBILITY;
  2760 
  2761 * HOL: got rid of some global declarations (potential INCOMPATIBILITY
  2762 for ML tools): const "()" renamed "Product_Type.Unity", type "unit"
  2763 renamed "Product_Type.unit";
  2764 
  2765 * HOL: renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
  2766 
  2767 * HOL: removed obsolete theorem "optionE" (use "option.exhaust", or
  2768 the "cases" method);
  2769 
  2770 * HOL/GroupTheory: group theory examples including Sylow's theorem (by
  2771 Florian Kammller);
  2772 
  2773 * HOL/IMP: updated and converted to new-style theory format; several
  2774 parts turned into readable document, with proper Isar proof texts and
  2775 some explanations (by Gerwin Klein);
  2776 
  2777 * HOL-Real: added Complex_Numbers (by Gertrud Bauer);
  2778 
  2779 * HOL-Hyperreal is now a logic image;
  2780 
  2781 
  2782 *** HOLCF ***
  2783 
  2784 * Isar: consts/constdefs supports mixfix syntax for continuous
  2785 operations;
  2786 
  2787 * Isar: domain package adapted to new-style theory format, e.g. see
  2788 HOLCF/ex/Dnat.thy;
  2789 
  2790 * theory Lift: proper use of rep_datatype lift instead of ML hacks --
  2791 potential INCOMPATIBILITY; now use plain induct_tac instead of former
  2792 lift.induct_tac, always use UU instead of Undef;
  2793 
  2794 * HOLCF/IMP: updated and converted to new-style theory;
  2795 
  2796 
  2797 *** ZF ***
  2798 
  2799 * Isar: proper integration of logic-specific tools and packages,
  2800 including theory commands '(co)inductive', '(co)datatype',
  2801 'rep_datatype', 'inductive_cases', as well as methods 'ind_cases',
  2802 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
  2803 
  2804 * theory Main no longer includes AC; for the Axiom of Choice, base
  2805 your theory on Main_ZFC;
  2806 
  2807 * the integer library now covers quotients and remainders, with many
  2808 laws relating division to addition, multiplication, etc.;
  2809 
  2810 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
  2811 typeless version of the formalism;
  2812 
  2813 * ZF/AC, Coind, IMP, Resid: updated and converted to new-style theory
  2814 format;
  2815 
  2816 * ZF/Induct: new directory for examples of inductive definitions,
  2817 including theory Multiset for multiset orderings; converted to
  2818 new-style theory format;
  2819 
  2820 * ZF: many new theorems about lists, ordinals, etc.;
  2821 
  2822 
  2823 *** General ***
  2824 
  2825 * Pure/kernel: meta-level proof terms (by Stefan Berghofer); reference
  2826 variable proof controls level of detail: 0 = no proofs (only oracle
  2827 dependencies), 1 = lemma dependencies, 2 = compact proof terms; see
  2828 also ref manual for further ML interfaces;
  2829 
  2830 * Pure/axclass: removed obsolete ML interface
  2831 goal_subclass/goal_arity;
  2832 
  2833 * Pure/syntax: new token syntax "num" for plain numerals (without "#"
  2834 of "xnum"); potential INCOMPATIBILITY, since -0, -1 etc. are now
  2835 separate tokens, so expressions involving minus need to be spaced
  2836 properly;
  2837 
  2838 * Pure/syntax: support non-oriented infixes, using keyword "infix"
  2839 rather than "infixl" or "infixr";
  2840 
  2841 * Pure/syntax: concrete syntax for dummy type variables admits genuine
  2842 sort constraint specifications in type inference; e.g. "x::_::foo"
  2843 ensures that the type of "x" is of sort "foo" (but not necessarily a
  2844 type variable);
  2845 
  2846 * Pure/syntax: print modes "type_brackets" and "no_type_brackets"
  2847 control output of nested => (types); the default behavior is
  2848 "type_brackets";
  2849 
  2850 * Pure/syntax: builtin parse translation for "_constify" turns valued
  2851 tokens into AST constants;
  2852 
  2853 * Pure/syntax: prefer later declarations of translations and print
  2854 translation functions; potential INCOMPATIBILITY: need to reverse
  2855 multiple declarations for same syntax element constant;
  2856 
  2857 * Pure/show_hyps reset by default (in accordance to existing Isar
  2858 practice);
  2859 
  2860 * Provers/classical: renamed addaltern to addafter, addSaltern to
  2861 addSafter;
  2862 
  2863 * Provers/clasimp: ``iff'' declarations now handle conditional rules
  2864 as well;
  2865 
  2866 * system: tested support for MacOS X; should be able to get Isabelle +
  2867 Proof General to work in a plain Terminal after installing Poly/ML
  2868 (e.g. from the Isabelle distribution area) and GNU bash alone
  2869 (e.g. from http://www.apple.com); full X11, XEmacs and X-Symbol
  2870 support requires further installations, e.g. from
  2871 http://fink.sourceforge.net/);
  2872 
  2873 * system: support Poly/ML 4.1.1 (able to manage larger heaps);
  2874 
  2875 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead
  2876 of 40 MB), cf. ML_OPTIONS;
  2877 
  2878 * system: Proof General keywords specification is now part of the
  2879 Isabelle distribution (see etc/isar-keywords.el);
  2880 
  2881 * system: support for persistent Proof General sessions (refrain from
  2882 outdating all loaded theories on startup); user may create writable
  2883 logic images like this: ``isabelle -q HOL Test'';
  2884 
  2885 * system: smart selection of Isabelle process versus Isabelle
  2886 interface, accommodates case-insensitive file systems (e.g. HFS+); may
  2887 run both "isabelle" and "Isabelle" even if file names are badly
  2888 damaged (executable inspects the case of the first letter of its own
  2889 name); added separate "isabelle-process" and "isabelle-interface";
  2890 
  2891 * system: refrain from any attempt at filtering input streams; no
  2892 longer support ``8bit'' encoding of old isabelle font, instead proper
  2893 iso-latin characters may now be used; the related isatools
  2894 "symbolinput" and "nonascii" have disappeared as well;
  2895 
  2896 * system: removed old "xterm" interface (the print modes "xterm" and
  2897 "xterm_color" are still available for direct use in a suitable
  2898 terminal);
  2899 
  2900 
  2901 
  2902 New in Isabelle99-2 (February 2001)
  2903 -----------------------------------
  2904 
  2905 *** Overview of INCOMPATIBILITIES ***
  2906 
  2907 * HOL: please note that theories in the Library and elsewhere often use the
  2908 new-style (Isar) format; to refer to their theorems in an ML script you must
  2909 bind them to ML identifers by e.g.      val thm_name = thm "thm_name";
  2910 
  2911 * HOL: inductive package no longer splits induction rule aggressively,
  2912 but only as far as specified by the introductions given; the old
  2913 format may be recovered via ML function complete_split_rule or attribute
  2914 'split_rule (complete)';
  2915 
  2916 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
  2917 gfp_Tarski to gfp_unfold;
  2918 
  2919 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
  2920 
  2921 * HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
  2922 relation); infix "^^" has been renamed "``"; infix "``" has been
  2923 renamed "`"; "univalent" has been renamed "single_valued";
  2924 
  2925 * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
  2926 operation;
  2927 
  2928 * HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
  2929 
  2930 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
  2931 
  2932 * Isar/HOL: method 'induct' now handles non-atomic goals; as a
  2933 consequence, it is no longer monotonic wrt. the local goal context
  2934 (which is now passed through the inductive cases);
  2935 
  2936 * Document preparation: renamed standard symbols \<ll> to \<lless> and
  2937 \<gg> to \<ggreater>;
  2938 
  2939 
  2940 *** Document preparation ***
  2941 
  2942 * \isabellestyle{NAME} selects version of Isabelle output (currently
  2943 available: are "it" for near math-mode best-style output, "sl" for
  2944 slanted text style, and "tt" for plain type-writer; if no
  2945 \isabellestyle command is given, output is according to slanted
  2946 type-writer);
  2947 
  2948 * support sub/super scripts (for single symbols only), input syntax is
  2949 like this: "A\<^sup>*" or "A\<^sup>\<star>";
  2950 
  2951 * some more standard symbols; see Appendix A of the system manual for
  2952 the complete list of symbols defined in isabellesym.sty;
  2953 
  2954 * improved isabelle style files; more abstract symbol implementation
  2955 (should now use \isamath{...} and \isatext{...} in custom symbol
  2956 definitions);
  2957 
  2958 * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
  2959 state; Note that presentation of goal states does not conform to
  2960 actual human-readable proof documents.  Please do not include goal
  2961 states into document output unless you really know what you are doing!
  2962 
  2963 * proper indentation of antiquoted output with proportional LaTeX
  2964 fonts;
  2965 
  2966 * no_document ML operator temporarily disables LaTeX document
  2967 generation;
  2968 
  2969 * isatool unsymbolize tunes sources for plain ASCII communication;
  2970 
  2971 
  2972 *** Isar ***
  2973 
  2974 * Pure: Isar now suffers initial goal statements to contain unbound
  2975 schematic variables (this does not conform to actual readable proof
  2976 documents, due to unpredictable outcome and non-compositional proof
  2977 checking); users who know what they are doing may use schematic goals
  2978 for Prolog-style synthesis of proven results;
  2979 
  2980 * Pure: assumption method (an implicit finishing) now handles actual
  2981 rules as well;
  2982 
  2983 * Pure: improved 'obtain' --- moved to Pure, insert "that" into
  2984 initial goal, declare "that" only as Pure intro (only for single
  2985 steps); the "that" rule assumption may now be involved in implicit
  2986 finishing, thus ".." becomes a feasible for trivial obtains;
  2987 
  2988 * Pure: default proof step now includes 'intro_classes'; thus trivial
  2989 instance proofs may be performed by "..";
  2990 
  2991 * Pure: ?thesis / ?this / "..." now work for pure meta-level
  2992 statements as well;
  2993 
  2994 * Pure: more robust selection of calculational rules;
  2995 
  2996 * Pure: the builtin notion of 'finished' goal now includes the ==-refl
  2997 rule (as well as the assumption rule);
  2998 
  2999 * Pure: 'thm_deps' command visualizes dependencies of theorems and
  3000 lemmas, using the graph browser tool;
  3001 
  3002 * Pure: predict failure of "show" in interactive mode;
  3003 
  3004 * Pure: 'thms_containing' now takes actual terms as arguments;
  3005 
  3006 * HOL: improved method 'induct' --- now handles non-atomic goals
  3007 (potential INCOMPATIBILITY); tuned error handling;
  3008 
  3009 * HOL: cases and induct rules now provide explicit hints about the
  3010 number of facts to be consumed (0 for "type" and 1 for "set" rules);
  3011 any remaining facts are inserted into the goal verbatim;
  3012 
  3013 * HOL: local contexts (aka cases) may now contain term bindings as
  3014 well; the 'cases' and 'induct' methods new provide a ?case binding for
  3015 the result to be shown in each case;
  3016 
  3017 * HOL: added 'recdef_tc' command;
  3018 
  3019 * isatool convert assists in eliminating legacy ML scripts;
  3020 
  3021 
  3022 *** HOL ***
  3023 
  3024 * HOL/Library: a collection of generic theories to be used together
  3025 with main HOL; the theory loader path already includes this directory
  3026 by default; the following existing theories have been moved here:
  3027 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
  3028 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
  3029 
  3030 * HOL/Unix: "Some aspects of Unix file-system security", a typical
  3031 modelling and verification task performed in Isabelle/HOL +
  3032 Isabelle/Isar + Isabelle document preparation (by Markus Wenzel).
  3033 
  3034 * HOL/Algebra: special summation operator SUM no longer exists, it has
  3035 been replaced by setsum; infix 'assoc' now has priority 50 (like
  3036 'dvd'); axiom 'one_not_zero' has been moved from axclass 'ring' to
  3037 'domain', this makes the theory consistent with mathematical
  3038 literature;
  3039 
  3040 * HOL basics: added overloaded operations "inverse" and "divide"
  3041 (infix "/"), syntax for generic "abs" operation, generic summation
  3042 operator \<Sum>;
  3043 
  3044 * HOL/typedef: simplified package, provide more useful rules (see also
  3045 HOL/subset.thy);
  3046 
  3047 * HOL/datatype: induction rule for arbitrarily branching datatypes is
  3048 now expressed as a proper nested rule (old-style tactic scripts may
  3049 require atomize_strip_tac to cope with non-atomic premises);
  3050 
  3051 * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
  3052 to "split_conv" (old name still available for compatibility);
  3053 
  3054 * HOL: improved concrete syntax for strings (e.g. allows translation
  3055 rules with string literals);
  3056 
  3057 * HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals
  3058  and Fleuriot's mechanization of analysis, including the transcendental
  3059  functions for the reals;
  3060 
  3061 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
  3062 
  3063 
  3064 *** CTT ***
  3065 
  3066 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
  3067 "lam" is displayed as TWO lambda-symbols
  3068 
  3069 * CTT: theory Main now available, containing everything (that is, Bool
  3070 and Arith);
  3071 
  3072 
  3073 *** General ***
  3074 
  3075 * Pure: the Simplifier has been implemented properly as a derived rule
  3076 outside of the actual kernel (at last!); the overall performance
  3077 penalty in practical applications is about 50%, while reliability of
  3078 the Isabelle inference kernel has been greatly improved;
  3079 
  3080 * print modes "brackets" and "no_brackets" control output of nested =>
  3081 (types) and ==> (props); the default behaviour is "brackets";
  3082 
  3083 * Provers: fast_tac (and friends) now handle actual object-logic rules
  3084 as assumptions as well;
  3085 
  3086 * system: support Poly/ML 4.0;
  3087 
  3088 * system: isatool install handles KDE version 1 or 2;
  3089 
  3090 
  3091 
  3092 New in Isabelle99-1 (October 2000)
  3093 ----------------------------------
  3094 
  3095 *** Overview of INCOMPATIBILITIES ***
  3096 
  3097 * HOL: simplification of natural numbers is much changed; to partly
  3098 recover the old behaviour (e.g. to prevent n+n rewriting to #2*n)
  3099 issue the following ML commands:
  3100 
  3101   Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
  3102   Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
  3103 
  3104 * HOL: simplification no longer dives into case-expressions; this is
  3105 controlled by "t.weak_case_cong" for each datatype t;
  3106 
  3107 * HOL: nat_less_induct renamed to less_induct;
  3108 
  3109 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool
  3110 fixsome to patch .thy and .ML sources automatically;
  3111 
  3112   select_equality  -> some_equality
  3113   select_eq_Ex     -> some_eq_ex
  3114   selectI2EX       -> someI2_ex
  3115   selectI2         -> someI2
  3116   selectI          -> someI
  3117   select1_equality -> some1_equality
  3118   Eps_sym_eq       -> some_sym_eq_trivial
  3119   Eps_eq           -> some_eq_trivial
  3120 
  3121 * HOL: exhaust_tac on datatypes superceded by new generic case_tac;
  3122 
  3123 * HOL: removed obsolete theorem binding expand_if (refer to split_if
  3124 instead);
  3125 
  3126 * HOL: the recursion equations generated by 'recdef' are now called
  3127 f.simps instead of f.rules;
  3128 
  3129 * HOL: qed_spec_mp now also handles bounded ALL as well;
  3130 
  3131 * HOL: 0 is now overloaded, so the type constraint ":: nat" may
  3132 sometimes be needed;
  3133 
  3134 * HOL: the constant for "f``x" is now "image" rather than "op ``";
  3135 
  3136 * HOL: the constant for "f-``x" is now "vimage" rather than "op -``";
  3137 
  3138 * HOL: the disjoint sum is now "<+>" instead of "Plus"; the cartesian
  3139 product is now "<*>" instead of "Times"; the lexicographic product is
  3140 now "<*lex*>" instead of "**";
  3141 
  3142 * HOL: theory Sexp is now in HOL/Induct examples (it used to be part
  3143 of main HOL, but was unused); better use HOL's datatype package;
  3144 
  3145 * HOL: removed "symbols" syntax for constant "override" of theory Map;
  3146 the old syntax may be recovered as follows:
  3147 
  3148   syntax (symbols)
  3149     override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
  3150       (infixl "\\<oplus>" 100)
  3151 
  3152 * HOL/Real: "rabs" replaced by overloaded "abs" function;
  3153 
  3154 * HOL/ML: even fewer consts are declared as global (see theories Ord,
  3155 Lfp, Gfp, WF); this only affects ML packages that refer to const names
  3156 internally;
  3157 
  3158 * HOL and ZF: syntax for quotienting wrt an equivalence relation
  3159 changed from A/r to A//r;
  3160 
  3161 * ZF: new treatment of arithmetic (nat & int) may break some old
  3162 proofs;
  3163 
  3164 * Isar: renamed some attributes (RS -> THEN, simplify -> simplified,
  3165 rulify -> rule_format, elimify -> elim_format, ...);
  3166 
  3167 * Isar/Provers: intro/elim/dest attributes changed; renamed
  3168 intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one
  3169 should have to change intro!! to intro? only); replaced "delrule" by
  3170 "rule del";
  3171 
  3172 * Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
  3173 
  3174 * Provers: strengthened force_tac by using new first_best_tac;
  3175 
  3176 * LaTeX document preparation: several changes of isabelle.sty (see
  3177 lib/texinputs);
  3178 
  3179 
  3180 *** Document preparation ***
  3181 
  3182 * formal comments (text blocks etc.) in new-style theories may now
  3183 contain antiquotations of thm/prop/term/typ/text to be presented
  3184 according to latex print mode; concrete syntax is like this:
  3185 @{term[show_types] "f(x) = a + x"};
  3186 
  3187 * isatool mkdir provides easy setup of Isabelle session directories,
  3188 including proper document sources;
  3189 
  3190 * generated LaTeX sources are now deleted after successful run
  3191 (isatool document -c); may retain a copy somewhere else via -D option
  3192 of isatool usedir;
  3193 
  3194 * isatool usedir -D now lets isatool latex -o sty update the Isabelle
  3195 style files, achieving self-contained LaTeX sources and simplifying
  3196 LaTeX debugging;
  3197 
  3198 * old-style theories now produce (crude) LaTeX output as well;
  3199 
  3200 * browser info session directories are now self-contained (may be put
  3201 on WWW server seperately); improved graphs of nested sessions; removed
  3202 graph for 'all sessions';
  3203 
  3204 * several improvements in isabelle style files; \isabellestyle{it}
  3205 produces fake math mode output; \isamarkupheader is now \section by
  3206 default; see lib/texinputs/isabelle.sty etc.;
  3207 
  3208 
  3209 *** Isar ***
  3210 
  3211 * Isar/Pure: local results and corresponding term bindings are now
  3212 subject to Hindley-Milner polymorphism (similar to ML); this
  3213 accommodates incremental type-inference very nicely;
  3214 
  3215 * Isar/Pure: new derived language element 'obtain' supports
  3216 generalized existence reasoning;
  3217 
  3218 * Isar/Pure: new calculational elements 'moreover' and 'ultimately'
  3219 support accumulation of results, without applying any rules yet;
  3220 useful to collect intermediate results without explicit name
  3221 references, and for use with transitivity rules with more than 2
  3222 premises;
  3223 
  3224 * Isar/Pure: scalable support for case-analysis type proofs: new
  3225 'case' language element refers to local contexts symbolically, as
  3226 produced by certain proof methods; internally, case names are attached
  3227 to theorems as "tags";
  3228 
  3229 * Isar/Pure: theory command 'hide' removes declarations from
  3230 class/type/const name spaces;
  3231 
  3232 * Isar/Pure: theory command 'defs' supports option "(overloaded)" to
  3233 indicate potential overloading;
  3234 
  3235 * Isar/Pure: changed syntax of local blocks from {{ }} to { };
  3236 
  3237 * Isar/Pure: syntax of sorts made 'inner', i.e. have to write
  3238 "{a,b,c}" instead of {a,b,c};
  3239 
  3240 * Isar/Pure now provides its own version of intro/elim/dest
  3241 attributes; useful for building new logics, but beware of confusion
  3242 with the version in Provers/classical;
  3243 
  3244 * Isar/Pure: the local context of (non-atomic) goals is provided via
  3245 case name 'antecedent';
  3246 
  3247 * Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms
  3248 to the current context is now done automatically);
  3249 
  3250 * Isar/Pure: theory command 'method_setup' provides a simple interface
  3251 for definining proof methods in ML;
  3252 
  3253 * Isar/Provers: intro/elim/dest attributes changed; renamed
  3254 intro/intro!/intro!! flags to intro!/intro/intro? (INCOMPATIBILITY, in
  3255 most cases, one should have to change intro!! to intro? only);
  3256 replaced "delrule" by "rule del";
  3257 
  3258 * Isar/Provers: new 'hypsubst' method, plain 'subst' method and
  3259 'symmetric' attribute (the latter supercedes [RS sym]);
  3260 
  3261 * Isar/Provers: splitter support (via 'split' attribute and 'simp'
  3262 method modifier); 'simp' method: 'only:' modifier removes loopers as
  3263 well (including splits);
  3264 
  3265 * Isar/Provers: Simplifier and Classical methods now support all kind
  3266 of modifiers used in the past, including 'cong', 'iff', etc.
  3267 
  3268 * Isar/Provers: added 'fastsimp' and 'clarsimp' methods (combination
  3269 of Simplifier and Classical reasoner);
  3270 
  3271 * Isar/HOL: new proof method 'cases' and improved version of 'induct'
  3272 now support named cases; major packages (inductive, datatype, primrec,
  3273 recdef) support case names and properly name parameters;
  3274 
  3275 * Isar/HOL: new transitivity rules for substitution in inequalities --
  3276 monotonicity conditions are extracted to be proven at end of
  3277 calculations;
  3278 
  3279 * Isar/HOL: removed 'case_split' thm binding, should use 'cases' proof
  3280 method anyway;
  3281 
  3282 * Isar/HOL: removed old expand_if = split_if; theorems if_splits =
  3283 split_if split_if_asm; datatype package provides theorems foo.splits =
  3284 foo.split foo.split_asm for each datatype;
  3285 
  3286 * Isar/HOL: tuned inductive package, rename "intrs" to "intros"
  3287 (potential INCOMPATIBILITY), emulation of mk_cases feature for proof
  3288 scripts: new 'inductive_cases' command and 'ind_cases' method; (Note:
  3289 use "(cases (simplified))" method in proper proof texts);
  3290 
  3291 * Isar/HOL: added global 'arith_split' attribute for 'arith' method;
  3292 
  3293 * Isar: names of theorems etc. may be natural numbers as well;
  3294 
  3295 * Isar: 'pr' command: optional arguments for goals_limit and
  3296 ProofContext.prems_limit; no longer prints theory contexts, but only
  3297 proof states;
  3298 
  3299 * Isar: diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
  3300 additional print modes to be specified; e.g. "pr(latex)" will print
  3301 proof state according to the Isabelle LaTeX style;
  3302 
  3303 * Isar: improved support for emulating tactic scripts, including proof
  3304 methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac',
  3305 'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac'
  3306 (for HOL datatypes);
  3307 
  3308 * Isar: simplified (more robust) goal selection of proof methods: 1st
  3309 goal, all goals, or explicit goal specifier (tactic emulation); thus
  3310 'proof method scripts' have to be in depth-first order;
  3311 
  3312 * Isar: tuned 'let' syntax: replaced 'as' keyword by 'and';
  3313 
  3314 * Isar: removed 'help' command, which hasn't been too helpful anyway;
  3315 should instead use individual commands for printing items
  3316 (print_commands, print_methods etc.);
  3317 
  3318 * Isar: added 'nothing' --- the empty list of theorems;
  3319 
  3320 
  3321 *** HOL ***
  3322 
  3323 * HOL/MicroJava: formalization of a fragment of Java, together with a
  3324 corresponding virtual machine and a specification of its bytecode
  3325 verifier and a lightweight bytecode verifier, including proofs of
  3326 type-safety; by Gerwin Klein, Tobias Nipkow, David von Oheimb, and
  3327 Cornelia Pusch (see also the homepage of project Bali at
  3328 http://isabelle.in.tum.de/Bali/);
  3329 
  3330 * HOL/Algebra: new theory of rings and univariate polynomials, by
  3331 Clemens Ballarin;
  3332 
  3333 * HOL/NumberTheory: fundamental Theorem of Arithmetic, Chinese
  3334 Remainder Theorem, Fermat/Euler Theorem, Wilson's Theorem, by Thomas M
  3335 Rasmussen;
  3336 
  3337 * HOL/Lattice: fundamental concepts of lattice theory and order
  3338 structures, including duals, properties of bounds versus algebraic
  3339 laws, lattice operations versus set-theoretic ones, the Knaster-Tarski
  3340 Theorem for complete lattices etc.; may also serve as a demonstration
  3341 for abstract algebraic reasoning using axiomatic type classes, and
  3342 mathematics-style proof in Isabelle/Isar; by Markus Wenzel;
  3343 
  3344 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog, by David
  3345 von Oheimb;
  3346 
  3347 * HOL/IMPP: extension of IMP with local variables and mutually
  3348 recursive procedures, by David von Oheimb;
  3349 
  3350 * HOL/Lambda: converted into new-style theory and document;
  3351 
  3352 * HOL/ex/Multiquote: example of multiple nested quotations and
  3353 anti-quotations -- basically a generalized version of de-Bruijn
  3354 representation; very useful in avoiding lifting of operations;
  3355 
  3356 * HOL/record: added general record equality rule to simpset; fixed
  3357 select-update simplification procedure to handle extended records as
  3358 well; admit "r" as field name;
  3359 
  3360 * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
  3361 other numeric types and also as the identity of groups, rings, etc.;
  3362 
  3363 * HOL: new axclass plus_ac0 for addition with the AC-laws and 0 as identity.
  3364 Types nat and int belong to this axclass;
  3365 
  3366 * HOL: greatly improved simplification involving numerals of type nat, int, real:
  3367    (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
  3368    i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
  3369   two terms #m*u and #n*u are replaced by #(m+n)*u
  3370     (where #m, #n and u can implicitly be 1; this is simproc combine_numerals)
  3371   and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
  3372     or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
  3373 
  3374 * HOL: meson_tac is available (previously in ex/meson.ML); it is a
  3375 powerful prover for predicate logic but knows nothing of clasets; see
  3376 ex/mesontest.ML and ex/mesontest2.ML for example applications;
  3377 
  3378 * HOL: new version of "case_tac" subsumes both boolean case split and
  3379 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
  3380 exists, may define val exhaust_tac = case_tac for ad-hoc portability;
  3381 
  3382 * HOL: simplification no longer dives into case-expressions: only the
  3383 selector expression is simplified, but not the remaining arms; to
  3384 enable full simplification of case-expressions for datatype t, you may
  3385 remove t.weak_case_cong from the simpset, either globally (Delcongs
  3386 [thm"t.weak_case_cong"];) or locally (delcongs [...]).
  3387 
  3388 * HOL/recdef: the recursion equations generated by 'recdef' for
  3389 function 'f' are now called f.simps instead of f.rules; if all
  3390 termination conditions are proved automatically, these simplification
  3391 rules are added to the simpset, as in primrec; rules may be named
  3392 individually as well, resulting in a separate list of theorems for
  3393 each equation;
  3394 
  3395 * HOL/While is a new theory that provides a while-combinator. It
  3396 permits the definition of tail-recursive functions without the
  3397 provision of a termination measure. The latter is necessary once the
  3398 invariant proof rule for while is applied.
  3399 
  3400 * HOL: new (overloaded) notation for the set of elements below/above
  3401 some element: {..u}, {..u(}, {l..}, {)l..}. See theory SetInterval.
  3402 
  3403 * HOL: theorems impI, allI, ballI bound as "strip";
  3404 
  3405 * HOL: new tactic induct_thm_tac: thm -> string -> int -> tactic
  3406 induct_tac th "x1 ... xn" expects th to have a conclusion of the form
  3407 P v1 ... vn and abbreviates res_inst_tac [("v1","x1"),...,("vn","xn")] th;
  3408 
  3409 * HOL/Real: "rabs" replaced by overloaded "abs" function;
  3410 
  3411 * HOL: theory Sexp now in HOL/Induct examples (it used to be part of
  3412 main HOL, but was unused);
  3413 
  3414 * HOL: fewer consts declared as global (e.g. have to refer to
  3415 "Lfp.lfp" instead of "lfp" internally; affects ML packages only);
  3416 
  3417 * HOL: tuned AST representation of nested pairs, avoiding bogus output
  3418 in case of overlap with user translations (e.g. judgements over
  3419 tuples); (note that the underlying logical represenation is still
  3420 bogus);
  3421 
  3422 
  3423 *** ZF ***
  3424 
  3425 * ZF: simplification automatically cancels common terms in arithmetic
  3426 expressions over nat and int;
  3427 
  3428 * ZF: new treatment of nat to minimize type-checking: all operators
  3429 coerce their operands to a natural number using the function natify,
  3430 making the algebraic laws unconditional;
  3431 
  3432 * ZF: as above, for int: operators coerce their operands to an integer
  3433 using the function intify;
  3434 
  3435 * ZF: the integer library now contains many of the usual laws for the
  3436 orderings, including $<=, and monotonicity laws for $+ and $*;
  3437 
  3438 * ZF: new example ZF/ex/NatSum to demonstrate integer arithmetic
  3439 simplification;
  3440 
  3441 * FOL and ZF: AddIffs now available, giving theorems of the form P<->Q
  3442 to the simplifier and classical reasoner simultaneously;
  3443 
  3444 
  3445 *** General ***
  3446 
  3447 * Provers: blast_tac now handles actual object-logic rules as
  3448 assumptions; note that auto_tac uses blast_tac internally as well;
  3449 
  3450 * Provers: new functions rulify/rulify_no_asm: thm -> thm for turning
  3451 outer -->/All/Ball into ==>/!!; qed_spec_mp now uses rulify_no_asm;
  3452 
  3453 * Provers: delrules now handles destruct rules as well (no longer need
  3454 explicit make_elim);
  3455 
  3456 * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
  3457   [| inj ?f;          ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
  3458 use instead the strong form,
  3459   [| inj ?f; ~ ?W ==> ?f ?x = ?f ?y; ?x = ?y ==> ?W |] ==> ?W
  3460 in HOL, FOL and ZF the function cla_make_elim will create such rules
  3461 from destruct-rules;
  3462 
  3463 * Provers: Simplifier.easy_setup provides a fast path to basic
  3464 Simplifier setup for new object-logics;
  3465 
  3466 * Pure: AST translation rules no longer require constant head on LHS;
  3467 
  3468 * Pure: improved name spaces: ambiguous output is qualified; support
  3469 for hiding of names;
  3470 
  3471 * system: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, and
  3472 XSYMBOL_HOME; no longer need to do manual configuration in most
  3473 situations;
  3474 
  3475 * system: compression of ML heaps images may now be controlled via -c
  3476 option of isabelle and isatool usedir (currently only observed by
  3477 Poly/ML);
  3478 
  3479 * system: isatool installfonts may handle X-Symbol fonts as well (very
  3480 useful for remote X11);
  3481 
  3482 * system: provide TAGS file for Isabelle sources;
  3483 
  3484 * ML: infix 'OF' is a version of 'MRS' with more appropriate argument
  3485 order;
  3486 
  3487 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
  3488 timing flag supersedes proof_timing and Toplevel.trace;
  3489 
  3490 * ML: new combinators |>> and |>>> for incremental transformations
  3491 with secondary results (e.g. certain theory extensions):
  3492 
  3493 * ML: PureThy.add_defs gets additional argument to indicate potential
  3494 overloading (usually false);
  3495 
  3496 * ML: PureThy.add_thms/add_axioms/add_defs now return theorems as
  3497 results;
  3498 
  3499 
  3500 
  3501 New in Isabelle99 (October 1999)
  3502 --------------------------------
  3503 
  3504 *** Overview of INCOMPATIBILITIES (see below for more details) ***
  3505 
  3506 * HOL: The THEN and ELSE parts of conditional expressions (if P then x else y)
  3507 are no longer simplified.  (This allows the simplifier to unfold recursive
  3508 functional programs.)  To restore the old behaviour, declare
  3509 
  3510     Delcongs [if_weak_cong];
  3511 
  3512 * HOL: Removed the obsolete syntax "Compl A"; use -A for set
  3513 complement;
  3514 
  3515 * HOL: the predicate "inj" is now defined by translation to "inj_on";
  3516 
  3517 * HOL/datatype: mutual_induct_tac no longer exists --
  3518   use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
  3519 
  3520 * HOL/typedef: fixed type inference for representing set; type
  3521 arguments now have to occur explicitly on the rhs as type constraints;
  3522 
  3523 * ZF: The con_defs part of an inductive definition may no longer refer
  3524 to constants declared in the same theory;
  3525 
  3526 * HOL, ZF: the function mk_cases, generated by the inductive
  3527 definition package, has lost an argument.  To simplify its result, it
  3528 uses the default simpset instead of a supplied list of theorems.
  3529 
  3530 * HOL/List: the constructors of type list are now Nil and Cons;
  3531 
  3532 * Simplifier: the type of the infix ML functions
  3533         setSSolver addSSolver setSolver addSolver
  3534 is now  simpset * solver -> simpset  where `solver' is a new abstract type
  3535 for packaging solvers. A solver is created via
  3536         mk_solver: string -> (thm list -> int -> tactic) -> solver
  3537 where the string argument is only a comment.
  3538 
  3539 
  3540 *** Proof tools ***
  3541 
  3542 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a
  3543 decision procedure for linear arithmetic. Currently it is used for
  3544 types `nat', `int', and `real' in HOL (see below); it can, should and
  3545 will be instantiated for other types and logics as well.
  3546 
  3547 * The simplifier now accepts rewrite rules with flexible heads, eg
  3548      hom ?f ==> ?f(?x+?y) = ?f ?x + ?f ?y
  3549   They are applied like any rule with a non-pattern lhs, i.e. by first-order
  3550   matching.
  3551 
  3552 
  3553 *** General ***
  3554 
  3555 * New Isabelle/Isar subsystem provides an alternative to traditional
  3556 tactical theorem proving; together with the ProofGeneral/isar user
  3557 interface it offers an interactive environment for developing human
  3558 readable proof documents (Isar == Intelligible semi-automated
  3559 reasoning); for further information see isatool doc isar-ref,
  3560 src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/
  3561 
  3562 * improved and simplified presentation of theories: better HTML markup
  3563 (including colors), graph views in several sizes; isatool usedir now
  3564 provides a proper interface for user theories (via -P option); actual
  3565 document preparation based on (PDF)LaTeX is available as well (for
  3566 new-style theories only); see isatool doc system for more information;
  3567 
  3568 * native support for Proof General, both for classic Isabelle and
  3569 Isabelle/Isar;
  3570 
  3571 * ML function thm_deps visualizes dependencies of theorems and lemmas,
  3572 using the graph browser tool;
  3573 
  3574 * Isabelle manuals now also available as PDF;
  3575 
  3576 * theory loader rewritten from scratch (may not be fully
  3577 bug-compatible); old loadpath variable has been replaced by show_path,
  3578 add_path, del_path, reset_path functions; new operations such as
  3579 update_thy, touch_thy, remove_thy, use/update_thy_only (see also
  3580 isatool doc ref);
  3581 
  3582 * improved isatool install: option -k creates KDE application icon,
  3583 option -p DIR installs standalone binaries;
  3584 
  3585 * added ML_PLATFORM setting (useful for cross-platform installations);
  3586 more robust handling of platform specific ML images for SML/NJ;
  3587 
  3588 * the settings environment is now statically scoped, i.e. it is never
  3589 created again in sub-processes invoked from isabelle, isatool, or
  3590 Isabelle;
  3591 
  3592 * path element specification '~~' refers to '$ISABELLE_HOME';
  3593 
  3594 * in locales, the "assumes" and "defines" parts may be omitted if
  3595 empty;
  3596 
  3597 * new print_mode "xsymbols" for extended symbol support (e.g. genuine
  3598 long arrows);
  3599 
  3600 * new print_mode "HTML";
  3601 
  3602 * new flag show_tags controls display of tags of theorems (which are
  3603 basically just comments that may be attached by some tools);
  3604 
  3605 * Isamode 2.6 requires patch to accomodate change of Isabelle font
  3606 mode and goal output format:
  3607 
  3608 diff -r Isamode-2.6/elisp/isa-load.el Isamode/elisp/isa-load.el
  3609 244c244
  3610 <       (list (isa-getenv "ISABELLE") "-msymbols" logic-name)
  3611 ---
  3612 >       (list (isa-getenv "ISABELLE") "-misabelle_font" "-msymbols" logic-name)
  3613 diff -r Isabelle-2.6/elisp/isa-proofstate.el Isamode/elisp/isa-proofstate.el
  3614 181c181
  3615 < (defconst proofstate-proofstart-regexp "^Level [0-9]+$"
  3616 ---
  3617 > (defconst proofstate-proofstart-regexp "^Level [0-9]+"
  3618 
  3619 * function bind_thms stores lists of theorems (cf. bind_thm);
  3620 
  3621 * new shorthand tactics ftac, eatac, datac, fatac;
  3622 
  3623 * qed (and friends) now accept "" as result name; in that case the
  3624 theorem is not stored, but proper checks and presentation of the
  3625 result still apply;
  3626 
  3627 * theorem database now also indexes constants "Trueprop", "all",
  3628 "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
  3629 
  3630 
  3631 *** HOL ***
  3632 
  3633 ** HOL arithmetic **
  3634 
  3635 * There are now decision procedures for linear arithmetic over nat and
  3636 int:
  3637 
  3638 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=',
  3639 `+', `-', `Suc', `min', `max' and numerical constants; other subterms
  3640 are treated as atomic; subformulae not involving type `nat' or `int'
  3641 are ignored; quantified subformulae are ignored unless they are
  3642 positive universal or negative existential. The tactic has to be
  3643 invoked by hand and can be a little bit slow. In particular, the
  3644 running time is exponential in the number of occurrences of `min' and
  3645 `max', and `-' on `nat'.
  3646 
  3647 2. fast_arith_tac is a cut-down version of arith_tac: it only takes
  3648 (negated) (in)equalities among the premises and the conclusion into
  3649 account (i.e. no compound formulae) and does not know about `min' and
  3650 `max', and `-' on `nat'. It is fast and is used automatically by the
  3651 simplifier.
  3652 
  3653 NB: At the moment, these decision procedures do not cope with mixed
  3654 nat/int formulae where the two parts interact, such as `m < n ==>
  3655 int(m) < int(n)'.
  3656 
  3657 * HOL/Numeral provides a generic theory of numerals (encoded
  3658 efficiently as bit strings); setup for types nat/int/real is in place;
  3659 INCOMPATIBILITY: since numeral syntax is now polymorphic, rather than
  3660 int, existing theories and proof scripts may require a few additional
  3661 type constraints;
  3662 
  3663 * integer division and remainder can now be performed on constant
  3664 arguments;
  3665 
  3666 * many properties of integer multiplication, division and remainder
  3667 are now available;
  3668 
  3669 * An interface to the Stanford Validity Checker (SVC) is available through the
  3670 tactic svc_tac.  Propositional tautologies and theorems of linear arithmetic
  3671 are proved automatically.  SVC must be installed separately, and its results
  3672 must be TAKEN ON TRUST (Isabelle does not check the proofs, but tags any
  3673 invocation of the underlying oracle).  For SVC see
  3674   http://verify.stanford.edu/SVC
  3675 
  3676 * IsaMakefile: the HOL-Real target now builds an actual image;
  3677 
  3678 
  3679 ** HOL misc **
  3680 
  3681 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces
  3682 (in Isabelle/Isar) -- by Gertrud Bauer;
  3683 
  3684 * HOL/BCV: generic model of bytecode verification, i.e. data-flow
  3685 analysis for assembly languages with subtypes;
  3686 
  3687 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization
  3688 -- avoids syntactic ambiguities and treats state, transition, and
  3689 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
  3690 changed syntax and (many) tactics;
  3691 
  3692 * HOL/inductive: Now also handles more general introduction rules such
  3693   as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
  3694   theorems are now maintained within the theory (maintained via the
  3695   "mono" attribute);
  3696 
  3697 * HOL/datatype: Now also handles arbitrarily branching datatypes
  3698   (using function types) such as
  3699 
  3700   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
  3701 
  3702 * HOL/record: record_simproc (part of the default simpset) takes care
  3703 of selectors applied to updated records; record_split_tac is no longer
  3704 part of the default claset; update_defs may now be removed from the
  3705 simpset in many cases; COMPATIBILITY: old behavior achieved by
  3706 
  3707   claset_ref () := claset() addSWrapper record_split_wrapper;
  3708   Delsimprocs [record_simproc]
  3709 
  3710 * HOL/typedef: fixed type inference for representing set; type
  3711 arguments now have to occur explicitly on the rhs as type constraints;
  3712 
  3713 * HOL/recdef (TFL): 'congs' syntax now expects comma separated list of theorem
  3714 names rather than an ML expression;
  3715 
  3716 * HOL/defer_recdef (TFL): like recdef but the well-founded relation can be
  3717 supplied later.  Program schemes can be defined, such as
  3718     "While B C s = (if B s then While B C (C s) else s)"
  3719 where the well-founded relation can be chosen after B and C have been given.
  3720 
  3721 * HOL/List: the constructors of type list are now Nil and Cons;
  3722 INCOMPATIBILITY: while [] and infix # syntax is still there, of
  3723 course, ML tools referring to List.list.op # etc. have to be adapted;
  3724 
  3725 * HOL_quantifiers flag superseded by "HOL" print mode, which is
  3726 disabled by default; run isabelle with option -m HOL to get back to
  3727 the original Gordon/HOL-style output;
  3728 
  3729 * HOL/Ord.thy: new bounded quantifier syntax (input only): ALL x<y. P,
  3730 ALL x<=y. P, EX x<y. P, EX x<=y. P;
  3731 
  3732 * HOL basic syntax simplified (more orthogonal): all variants of
  3733 All/Ex now support plain / symbolic / HOL notation; plain syntax for
  3734 Eps operator is provided as well: "SOME x. P[x]";
  3735 
  3736 * HOL/Sum.thy: sum_case has been moved to HOL/Datatype;
  3737 
  3738 * HOL/Univ.thy: infix syntax <*>, <+>, <**>, <+> eliminated and made
  3739 thus available for user theories;
  3740 
  3741 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with
  3742 HOL/List; hardly an INCOMPATIBILITY since '>>' syntax is used all the
  3743 time;
  3744 
  3745 * HOL: new tactic smp_tac: int -> int -> tactic, which applies spec
  3746 several times and then mp;
  3747 
  3748 
  3749 *** LK ***
  3750 
  3751 * the notation <<...>> is now available as a notation for sequences of
  3752 formulas;
  3753 
  3754 * the simplifier is now installed
  3755 
  3756 * the axiom system has been generalized (thanks to Soren Heilmann)
  3757 
  3758 * the classical reasoner now has a default rule database
  3759 
  3760 
  3761 *** ZF ***
  3762 
  3763 * new primrec section allows primitive recursive functions to be given
  3764 directly (as in HOL) over datatypes and the natural numbers;
  3765 
  3766 * new tactics induct_tac and exhaust_tac for induction (or case
  3767 analysis) over datatypes and the natural numbers;
  3768 
  3769 * the datatype declaration of type T now defines the recursor T_rec;
  3770 
  3771 * simplification automatically does freeness reasoning for datatype
  3772 constructors;
  3773 
  3774 * automatic type-inference, with AddTCs command to insert new
  3775 type-checking rules;
  3776 
  3777 * datatype introduction rules are now added as Safe Introduction rules
  3778 to the claset;
  3779 
  3780 * the syntax "if P then x else y" is now available in addition to
  3781 if(P,x,y);
  3782 
  3783 
  3784 *** Internal programming interfaces ***
  3785 
  3786 * tuned simplifier trace output; new flag debug_simp;
  3787 
  3788 * structures Vartab / Termtab (instances of TableFun) offer efficient
  3789 tables indexed by indexname_ord / term_ord (compatible with aconv);
  3790 
  3791 * AxClass.axclass_tac lost the theory argument;
  3792 
  3793 * tuned current_goals_markers semantics: begin / end goal avoids
  3794 printing empty lines;
  3795 
  3796 * removed prs and prs_fn hook, which was broken because it did not
  3797 include \n in its semantics, forcing writeln to add one
  3798 uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
  3799 string -> unit if you really want to output text without newline;
  3800 
  3801 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to
  3802 plain output, interface builders may have to enable 'isabelle_font'
  3803 mode to get Isabelle font glyphs as before;
  3804 
  3805 * refined token_translation interface; INCOMPATIBILITY: output length
  3806 now of type real instead of int;
  3807 
  3808 * theory loader actions may be traced via new ThyInfo.add_hook
  3809 interface (see src/Pure/Thy/thy_info.ML); example application: keep
  3810 your own database of information attached to *whole* theories -- as
  3811 opposed to intra-theory data slots offered via TheoryDataFun;
  3812 
  3813 * proper handling of dangling sort hypotheses (at last!);
  3814 Thm.strip_shyps and Drule.strip_shyps_warning take care of removing
  3815 extra sort hypotheses that can be witnessed from the type signature;
  3816 the force_strip_shyps flag is gone, any remaining shyps are simply
  3817 left in the theorem (with a warning issued by strip_shyps_warning);
  3818 
  3819 
  3820 
  3821 New in Isabelle98-1 (October 1998)
  3822 ----------------------------------
  3823 
  3824 *** Overview of INCOMPATIBILITIES (see below for more details) ***
  3825 
  3826 * several changes of automated proof tools;
  3827 
  3828 * HOL: major changes to the inductive and datatype packages, including
  3829 some minor incompatibilities of theory syntax;
  3830 
  3831 * HOL: renamed r^-1 to 'converse' from 'inverse'; 'inj_onto' is now
  3832 called `inj_on';
  3833 
  3834 * HOL: removed duplicate thms in Arith:
  3835   less_imp_add_less  should be replaced by  trans_less_add1
  3836   le_imp_add_le      should be replaced by  trans_le_add1
  3837 
  3838 * HOL: unary minus is now overloaded (new type constraints may be
  3839 required);
  3840 
  3841 * HOL and ZF: unary minus for integers is now #- instead of #~.  In
  3842 ZF, expressions such as n#-1 must be changed to n#- 1, since #-1 is
  3843 now taken as an integer constant.
  3844 
  3845 * Pure: ML function 'theory_of' renamed to 'theory';
  3846 
  3847 
  3848 *** Proof tools ***
  3849 
  3850 * Simplifier:
  3851   1. Asm_full_simp_tac is now more aggressive.
  3852      1. It will sometimes reorient premises if that increases their power to
  3853         simplify.
  3854      2. It does no longer proceed strictly from left to right but may also
  3855         rotate premises to achieve further simplification.
  3856      For compatibility reasons there is now Asm_lr_simp_tac which is like the
  3857      old Asm_full_simp_tac in that it does not rotate premises.
  3858   2. The simplifier now knows a little bit about nat-arithmetic.
  3859 
  3860 * Classical reasoner: wrapper mechanism for the classical reasoner now
  3861 allows for selected deletion of wrappers, by introduction of names for
  3862 wrapper functionals.  This implies that addbefore, addSbefore,
  3863 addaltern, and addSaltern now take a pair (name, tactic) as argument,
  3864 and that adding two tactics with the same name overwrites the first
  3865 one (emitting a warning).
  3866   type wrapper = (int -> tactic) -> (int -> tactic)
  3867   setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
  3868   addWrapper, addSWrapper: claset * (string * wrapper) -> claset
  3869   delWrapper, delSWrapper: claset *  string            -> claset
  3870   getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
  3871 
  3872 * Classical reasoner: addbefore/addSbefore now have APPEND/ORELSE
  3873 semantics; addbefore now affects only the unsafe part of step_tac
  3874 etc.; this affects addss/auto_tac/force_tac, so EXISTING PROOFS MAY
  3875 FAIL, but proofs should be fixable easily, e.g. by replacing Auto_tac
  3876 by Force_tac;
  3877 
  3878 * Classical reasoner: setwrapper to setWrapper and compwrapper to
  3879 compWrapper; added safe wrapper (and access functions for it);
  3880 
  3881 * HOL/split_all_tac is now much faster and fails if there is nothing
  3882 to split.  Some EXISTING PROOFS MAY REQUIRE ADAPTION because the order
  3883 and the names of the automatically generated variables have changed.
  3884 split_all_tac has moved within claset() from unsafe wrappers to safe
  3885 wrappers, which means that !!-bound variables are split much more
  3886 aggressively, and safe_tac and clarify_tac now split such variables.
  3887 If this splitting is not appropriate, use delSWrapper "split_all_tac".
  3888 Note: the same holds for record_split_tac, which does the job of
  3889 split_all_tac for record fields.
  3890 
  3891 * HOL/Simplifier: Rewrite rules for case distinctions can now be added
  3892 permanently to the default simpset using Addsplits just like
  3893 Addsimps. They can be removed via Delsplits just like
  3894 Delsimps. Lower-case versions are also available.
  3895 
  3896 * HOL/Simplifier: The rule split_if is now part of the default
  3897 simpset. This means that the simplifier will eliminate all occurrences
  3898 of if-then-else in the conclusion of a goal. To prevent this, you can
  3899 either remove split_if completely from the default simpset by
  3900 `Delsplits [split_if]' or remove it in a specific call of the
  3901 simplifier using `... delsplits [split_if]'.  You can also add/delete
  3902 other case splitting rules to/from the default simpset: every datatype
  3903 generates suitable rules `split_t_case' and `split_t_case_asm' (where
  3904 t is the name of the datatype).
  3905 
  3906 * Classical reasoner / Simplifier combination: new force_tac (and
  3907 derivatives Force_tac, force) combines rewriting and classical
  3908 reasoning (and whatever other tools) similarly to auto_tac, but is
  3909 aimed to solve the given subgoal completely.
  3910 
  3911 
  3912 *** General ***
  3913 
  3914 * new top-level commands `Goal' and `Goalw' that improve upon `goal'
  3915 and `goalw': the theory is no longer needed as an explicit argument -
  3916 the current theory context is used; assumptions are no longer returned
  3917 at the ML-level unless one of them starts with ==> or !!; it is
  3918 recommended to convert to these new commands using isatool fixgoal
  3919 (backup your sources first!);
  3920 
  3921 * new top-level commands 'thm' and 'thms' for retrieving theorems from
  3922 the current theory context, and 'theory' to lookup stored theories;
  3923 
  3924 * new theory section 'locale' for declaring constants, assumptions and
  3925 definitions that have local scope;
  3926 
  3927 * new theory section 'nonterminals' for purely syntactic types;
  3928 
  3929 * new theory section 'setup' for generic ML setup functions
  3930 (e.g. package initialization);
  3931 
  3932 * the distribution now includes Isabelle icons: see
  3933 lib/logo/isabelle-{small,tiny}.xpm;
  3934 
  3935 * isatool install - install binaries with absolute references to
  3936 ISABELLE_HOME/bin;
  3937 
  3938 * isatool logo -- create instances of the Isabelle logo (as EPS);
  3939 
  3940 * print mode 'emacs' reserved for Isamode;
  3941 
  3942 * support multiple print (ast) translations per constant name;
  3943 
  3944 * theorems involving oracles are now printed with a suffixed [!];
  3945 
  3946 
  3947 *** HOL ***
  3948 
  3949 * there is now a tutorial on Isabelle/HOL (do 'isatool doc tutorial');
  3950 
  3951 * HOL/inductive package reorganized and improved: now supports mutual
  3952 definitions such as
  3953 
  3954   inductive EVEN ODD
  3955     intrs
  3956       null "0 : EVEN"
  3957       oddI "n : EVEN ==> Suc n : ODD"
  3958       evenI "n : ODD ==> Suc n : EVEN"
  3959 
  3960 new theorem list "elims" contains an elimination rule for each of the
  3961 recursive sets; inductive definitions now handle disjunctive premises
  3962 correctly (also ZF);
  3963 
  3964 INCOMPATIBILITIES: requires Inductive as an ancestor; component
  3965 "mutual_induct" no longer exists - the induction rule is always
  3966 contained in "induct";
  3967 
  3968 
  3969 * HOL/datatype package re-implemented and greatly improved: now
  3970 supports mutually recursive datatypes such as
  3971 
  3972   datatype
  3973     'a aexp = IF_THEN_ELSE ('a bexp) ('a aexp) ('a aexp)
  3974             | SUM ('a aexp) ('a aexp)
  3975             | DIFF ('a aexp) ('a aexp)
  3976             | NUM 'a
  3977   and
  3978     'a bexp = LESS ('a aexp) ('a aexp)
  3979             | AND ('a bexp) ('a bexp)
  3980             | OR ('a bexp) ('a bexp)
  3981 
  3982 as well as indirectly recursive datatypes such as
  3983 
  3984   datatype
  3985     ('a, 'b) term = Var 'a
  3986                   | App 'b ((('a, 'b) term) list)
  3987 
  3988 The new tactic  mutual_induct_tac [<var_1>, ..., <var_n>] i  performs
  3989 induction on mutually / indirectly recursive datatypes.
  3990 
  3991 Primrec equations are now stored in theory and can be accessed via
  3992 <function_name>.simps.
  3993 
  3994 INCOMPATIBILITIES:
  3995 
  3996   - Theories using datatypes must now have theory Datatype as an
  3997     ancestor.
  3998   - The specific <typename>.induct_tac no longer exists - use the
  3999     generic induct_tac instead.
  4000   - natE has been renamed to nat.exhaust - use exhaust_tac
  4001     instead of res_inst_tac ... natE. Note that the variable
  4002     names in nat.exhaust differ from the names in natE, this
  4003     may cause some "fragile" proofs to fail.
  4004   - The theorems split_<typename>_case and split_<typename>_case_asm
  4005     have been renamed to <typename>.split and <typename>.split_asm.
  4006   - Since default sorts of type variables are now handled correctly,
  4007     some datatype definitions may have to be annotated with explicit
  4008     sort constraints.
  4009   - Primrec definitions no longer require function name and type
  4010     of recursive argument.
  4011 
  4012 Consider using isatool fixdatatype to adapt your theories and proof
  4013 scripts to the new package (backup your sources first!).
  4014 
  4015 
  4016 * HOL/record package: considerably improved implementation; now
  4017 includes concrete syntax for record types, terms, updates; theorems
  4018 for surjective pairing and splitting !!-bound record variables; proof
  4019 support is as follows:
  4020 
  4021   1) standard conversions (selectors or updates applied to record
  4022 constructor terms) are part of the standard simpset;
  4023 
  4024   2) inject equations of the form ((x, y) = (x', y')) == x=x' & y=y' are
  4025 made part of standard simpset and claset via addIffs;
  4026 
  4027   3) a tactic for record field splitting (record_split_tac) is part of
  4028 the standard claset (addSWrapper);
  4029 
  4030 To get a better idea about these rules you may retrieve them via
  4031 something like 'thms "foo.simps"' or 'thms "foo.iffs"', where "foo" is
  4032 the name of your record type.
  4033 
  4034 The split tactic 3) conceptually simplifies by the following rule:
  4035 
  4036   "(!!x. PROP ?P x) == (!!a b. PROP ?P (a, b))"
  4037 
  4038 Thus any record variable that is bound by meta-all will automatically
  4039 blow up into some record constructor term, consequently the
  4040 simplifications of 1), 2) apply.  Thus force_tac, auto_tac etc. shall
  4041 solve record problems automatically.
  4042 
  4043 
  4044 * reorganized the main HOL image: HOL/Integ and String loaded by
  4045 default; theory Main includes everything;
  4046 
  4047 * automatic simplification of integer sums and comparisons, using cancellation;
  4048 
  4049 * added option_map_eq_Some and not_Some_eq to the default simpset and claset;
  4050 
  4051 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset;
  4052 
  4053 * many new identities for unions, intersections, set difference, etc.;
  4054 
  4055 * expand_if, expand_split, expand_sum_case and expand_nat_case are now
  4056 called split_if, split_split, split_sum_case and split_nat_case (to go
  4057 with add/delsplits);
  4058 
  4059 * HOL/Prod introduces simplification procedure unit_eq_proc rewriting
  4060 (?x::unit) = (); this is made part of the default simpset, which COULD
  4061 MAKE EXISTING PROOFS FAIL under rare circumstances (consider
  4062 'Delsimprocs [unit_eq_proc];' as last resort); also note that
  4063 unit_abs_eta_conv is added in order to counter the effect of
  4064 unit_eq_proc on (%u::unit. f u), replacing it by f rather than by
  4065 %u.f();
  4066 
  4067 * HOL/Fun INCOMPATIBILITY: `inj_onto' is now called `inj_on' (which
  4068 makes more sense);
  4069 
  4070 * HOL/Set INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
  4071   It and 'sym RS equals0D' are now in the default  claset, giving automatic
  4072   disjointness reasoning but breaking a few old proofs.
  4073 
  4074 * HOL/Relation INCOMPATIBILITY: renamed the relational operator r^-1
  4075 to 'converse' from 'inverse' (for compatibility with ZF and some
  4076 literature);
  4077 
  4078 * HOL/recdef can now declare non-recursive functions, with {} supplied as
  4079 the well-founded relation;
  4080 
  4081 * HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
  4082     Compl A.  The "Compl" syntax remains available as input syntax for this
  4083     release ONLY.
  4084 
  4085 * HOL/Update: new theory of function updates:
  4086     f(a:=b) == %x. if x=a then b else f x
  4087 may also be iterated as in f(a:=b,c:=d,...);
  4088 
  4089 * HOL/Vimage: new theory for inverse image of a function, syntax f-``B;
  4090 
  4091 * HOL/List:
  4092   - new function list_update written xs[i:=v] that updates the i-th
  4093     list position. May also be iterated as in xs[i:=a,j:=b,...].
  4094   - new function `upt' written [i..j(] which generates the list
  4095     [i,i+1,...,j-1], i.e. the upper bound is excluded. To include the upper
  4096     bound write [i..j], which is a shorthand for [i..j+1(].
  4097   - new lexicographic orderings and corresponding wellfoundedness theorems.
  4098 
  4099 * HOL/Arith:
  4100   - removed 'pred' (predecessor) function;
  4101   - generalized some theorems about n-1;
  4102   - many new laws about "div" and "mod";
  4103   - new laws about greatest common divisors (see theory ex/Primes);
  4104 
  4105 * HOL/Relation: renamed the relational operator r^-1 "converse"
  4106 instead of "inverse";
  4107 
  4108 * HOL/Induct/Multiset: a theory of multisets, including the wellfoundedness
  4109   of the multiset ordering;
  4110 
  4111 * directory HOL/Real: a construction of the reals using Dedekind cuts
  4112   (not included by default);
  4113 
  4114 * directory HOL/UNITY: Chandy and Misra's UNITY formalism;
  4115 
  4116 * directory HOL/Hoare: a new version of Hoare logic which permits many-sorted
  4117   programs, i.e. different program variables may have different types.
  4118 
  4119 * calling (stac rew i) now fails if "rew" has no effect on the goal
  4120   [previously, this check worked only if the rewrite rule was unconditional]
  4121   Now rew can involve either definitions or equalities (either == or =).
  4122 
  4123 
  4124 *** ZF ***
  4125 
  4126 * theory Main includes everything; INCOMPATIBILITY: theory ZF.thy contains
  4127   only the theorems proved on ZF.ML;
  4128 
  4129 * ZF INCOMPATIBILITY: rule `equals0D' is now a well-formed destruct rule;
  4130   It and 'sym RS equals0D' are now in the default  claset, giving automatic
  4131   disjointness reasoning but breaking a few old proofs.
  4132 
  4133 * ZF/Update: new theory of function updates
  4134     with default rewrite rule  f(x:=y) ` z = if(z=x, y, f`z)
  4135   may also be iterated as in f(a:=b,c:=d,...);
  4136 
  4137 * in  let x=t in u(x), neither t nor u(x) has to be an FOL term.
  4138 
  4139 * calling (stac rew i) now fails if "rew" has no effect on the goal
  4140   [previously, this check worked only if the rewrite rule was unconditional]
  4141   Now rew can involve either definitions or equalities (either == or =).
  4142 
  4143 * case_tac provided for compatibility with HOL
  4144     (like the old excluded_middle_tac, but with subgoals swapped)
  4145 
  4146 
  4147 *** Internal programming interfaces ***
  4148 
  4149 * Pure: several new basic modules made available for general use, see
  4150 also src/Pure/README;
  4151 
  4152 * improved the theory data mechanism to support encapsulation (data
  4153 kind name replaced by private Object.kind, acting as authorization
  4154 key); new type-safe user interface via functor TheoryDataFun; generic
  4155 print_data function becomes basically useless;
  4156 
  4157 * removed global_names compatibility flag -- all theory declarations
  4158 are qualified by default;
  4159 
  4160 * module Pure/Syntax now offers quote / antiquote translation
  4161 functions (useful for Hoare logic etc. with implicit dependencies);
  4162 see HOL/ex/Antiquote for an example use;
  4163 
  4164 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
  4165 cterm -> thm;
  4166 
  4167 * new tactical CHANGED_GOAL for checking that a tactic modifies a
  4168 subgoal;
  4169 
  4170 * Display.print_goals function moved to Locale.print_goals;
  4171 
  4172 * standard print function for goals supports current_goals_markers
  4173 variable for marking begin of proof, end of proof, start of goal; the
  4174 default is ("", "", ""); setting current_goals_markers := ("<proof>",
  4175 "</proof>", "<goal>") causes SGML like tagged proof state printing,
  4176 for example;
  4177 
  4178 
  4179 
  4180 New in Isabelle98 (January 1998)
  4181 --------------------------------
  4182 
  4183 *** Overview of INCOMPATIBILITIES (see below for more details) ***
  4184 
  4185 * changed lexical syntax of terms / types: dots made part of long
  4186 identifiers, e.g. "%x.x" no longer possible, should be "%x. x";
  4187 
  4188 * simpset (and claset) reference variable replaced by functions
  4189 simpset / simpset_ref;
  4190 
  4191 * no longer supports theory aliases (via merge) and non-trivial
  4192 implicit merge of thms' signatures;
  4193 
  4194 * most internal names of constants changed due to qualified names;
  4195 
  4196 * changed Pure/Sequence interface (see Pure/seq.ML);
  4197 
  4198 
  4199 *** General Changes ***
  4200 
  4201 * hierachically structured name spaces (for consts, types, axms, thms
  4202 etc.); new lexical class 'longid' (e.g. Foo.bar.x) may render much of
  4203 old input syntactically incorrect (e.g. "%x.x"); COMPATIBILITY:
  4204 isatool fixdots ensures space after dots (e.g. "%x. x"); set
  4205 long_names for fully qualified output names; NOTE: ML programs
  4206 (special tactics, packages etc.) referring to internal names may have
  4207 to be adapted to cope with fully qualified names; in case of severe
  4208 backward campatibility problems try setting 'global_names' at compile
  4209 time to have enrything declared within a flat name space; one may also
  4210 fine tune name declarations in theories via the 'global' and 'local'
  4211 section;
  4212 
  4213 * reimplemented the implicit simpset and claset using the new anytype
  4214 data filed in signatures; references simpset:simpset ref etc. are
  4215 replaced by functions simpset:unit->simpset and
  4216 simpset_ref:unit->simpset ref; COMPATIBILITY: use isatool fixclasimp
  4217 to patch your ML files accordingly;
  4218 
  4219 * HTML output now includes theory graph data for display with Java
  4220 applet or isatool browser; data generated automatically via isatool
  4221 usedir (see -i option, ISABELLE_USEDIR_OPTIONS);
  4222 
  4223 * defs may now be conditional; improved rewrite_goals_tac to handle
  4224 conditional equations;
  4225 
  4226 * defs now admits additional type arguments, using TYPE('a) syntax;
  4227 
  4228 * theory aliases via merge (e.g. M=A+B+C) no longer supported, always
  4229 creates a new theory node; implicit merge of thms' signatures is
  4230 restricted to 'trivial' ones; COMPATIBILITY: one may have to use
  4231 transfer:theory->thm->thm in (rare) cases;
  4232 
  4233 * improved handling of draft signatures / theories; draft thms (and
  4234 ctyps, cterms) are automatically promoted to real ones;
  4235 
  4236 * slightly changed interfaces for oracles: admit many per theory, named
  4237 (e.g. oracle foo = mlfun), additional name argument for invoke_oracle;
  4238 
  4239 * print_goals: optional output of const types (set show_consts and
  4240 show_types);
  4241 
  4242 * improved output of warnings (###) and errors (***);
  4243 
  4244 * subgoal_tac displays a warning if the new subgoal has type variables;
  4245 
  4246 * removed old README and Makefiles;
  4247 
  4248 * replaced print_goals_ref hook by print_current_goals_fn and result_error_fn;
  4249 
  4250 * removed obsolete init_pps and init_database;
  4251 
  4252 * deleted the obsolete tactical STATE, which was declared by
  4253     fun STATE tacfun st = tacfun st st;
  4254 
  4255 * cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
  4256 (which abbreviates $HOME);
  4257 
  4258 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
  4259 use isatool fixseq to adapt your ML programs (this works for fully
  4260 qualified references to the Sequence structure only!);
  4261 
  4262 * use_thy no longer requires writable current directory; it always
  4263 reloads .ML *and* .thy file, if either one is out of date;
  4264 
  4265 
  4266 *** Classical Reasoner ***
  4267 
  4268 * Clarify_tac, clarify_tac, clarify_step_tac, Clarify_step_tac: new
  4269 tactics that use classical reasoning to simplify a subgoal without
  4270 splitting it into several subgoals;
  4271 
  4272 * Safe_tac: like safe_tac but uses the default claset;
  4273 
  4274 
  4275 *** Simplifier ***
  4276 
  4277 * added simplification meta rules:
  4278     (asm_)(full_)simplify: simpset -> thm -> thm;
  4279 
  4280 * simplifier.ML no longer part of Pure -- has to be loaded by object
  4281 logics (again);
  4282 
  4283 * added prems argument to simplification procedures;
  4284 
  4285 * HOL, FOL, ZF: added infix function `addsplits':
  4286   instead of `<simpset> setloop (split_tac <thms>)'
  4287   you can simply write `<simpset> addsplits <thms>'
  4288 
  4289 
  4290 *** Syntax ***
  4291 
  4292 * TYPE('a) syntax for type reflection terms;
  4293 
  4294 * no longer handles consts with name "" -- declare as 'syntax' instead;
  4295 
  4296 * pretty printer: changed order of mixfix annotation preference (again!);
  4297 
  4298 * Pure: fixed idt/idts vs. pttrn/pttrns syntactic categories;
  4299 
  4300 
  4301 *** HOL ***
  4302 
  4303 * HOL: there is a new splitter `split_asm_tac' that can be used e.g.
  4304   with `addloop' of the simplifier to faciliate case splitting in premises.
  4305 
  4306 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
  4307 
  4308 * HOL/Auth: new protocol proofs including some for the Internet
  4309   protocol TLS;
  4310 
  4311 * HOL/Map: new theory of `maps' a la VDM;
  4312 
  4313 * HOL/simplifier: simplification procedures nat_cancel_sums for
  4314 cancelling out common nat summands from =, <, <= (in)equalities, or
  4315 differences; simplification procedures nat_cancel_factor for
  4316 cancelling common factor from =, <, <= (in)equalities over natural
  4317 sums; nat_cancel contains both kinds of procedures, it is installed by
  4318 default in Arith.thy -- this COULD MAKE EXISTING PROOFS FAIL;
  4319 
  4320 * HOL/simplifier: terms of the form
  4321   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
  4322   are rewritten to
  4323   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t)',
  4324   and those of the form
  4325   `! x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x) --> R(x)'  (or t=x)
  4326   are rewritten to
  4327   `P1(t) & ... & Pn(t) & Q1(t) & ... Qn(t) --> R(t)',
  4328 
  4329 * HOL/datatype
  4330   Each datatype `t' now comes with a theorem `split_t_case' of the form
  4331 
  4332   P(t_case f1 ... fn x) =
  4333      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
  4334         ...
  4335        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
  4336      )
  4337 
  4338   and a theorem `split_t_case_asm' of the form
  4339 
  4340   P(t_case f1 ... fn x) =
  4341     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
  4342         ...
  4343        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
  4344      )
  4345   which can be added to a simpset via `addsplits'. The existing theorems
  4346   expand_list_case and expand_option_case have been renamed to
  4347   split_list_case and split_option_case.
  4348 
  4349 * HOL/Arithmetic:
  4350   - `pred n' is automatically converted to `n-1'.
  4351     Users are strongly encouraged not to use `pred' any longer,
  4352     because it will disappear altogether at some point.
  4353   - Users are strongly encouraged to write "0 < n" rather than
  4354     "n ~= 0". Theorems and proof tools have been modified towards this
  4355     `standard'.
  4356 
  4357 * HOL/Lists:
  4358   the function "set_of_list" has been renamed "set" (and its theorems too);
  4359   the function "nth" now takes its arguments in the reverse order and
  4360   has acquired the infix notation "!" as in "xs!n".
  4361 
  4362 * HOL/Set: UNIV is now a constant and is no longer translated to Compl{};
  4363 
  4364 * HOL/Set: The operator (UN x.B x) now abbreviates (UN x:UNIV. B x) and its
  4365   specialist theorems (like UN1_I) are gone.  Similarly for (INT x.B x);
  4366 
  4367 * HOL/record: extensible records with schematic structural subtyping
  4368 (single inheritance); EXPERIMENTAL version demonstrating the encoding,
  4369 still lacks various theorems and concrete record syntax;
  4370 
  4371 
  4372 *** HOLCF ***
  4373 
  4374 * removed "axioms" and "generated by" sections;
  4375 
  4376 * replaced "ops" section by extended "consts" section, which is capable of
  4377   handling the continuous function space "->" directly;
  4378 
  4379 * domain package:
  4380   . proves theorems immediately and stores them in the theory,
  4381   . creates hierachical name space,
  4382   . now uses normal mixfix annotations (instead of cinfix...),
  4383   . minor changes to some names and values (for consistency),
  4384   . e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas,
  4385   . separator between mutual domain defs: changed "," to "and",
  4386   . improved handling of sort constraints;  now they have to
  4387     appear on the left-hand side of the equations only;
  4388 
  4389 * fixed LAM <x,y,zs>.b syntax;
  4390 
  4391 * added extended adm_tac to simplifier in HOLCF -- can now discharge
  4392 adm (%x. P (t x)), where P is chainfinite and t continuous;
  4393 
  4394 
  4395 *** FOL and ZF ***
  4396 
  4397 * FOL: there is a new splitter `split_asm_tac' that can be used e.g.
  4398   with `addloop' of the simplifier to faciliate case splitting in premises.
  4399 
  4400 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
  4401 in HOL, they strip ALL and --> from proved theorems;
  4402 
  4403 
  4404 
  4405 New in Isabelle94-8 (May 1997)
  4406 ------------------------------
  4407 
  4408 *** General Changes ***
  4409 
  4410 * new utilities to build / run / maintain Isabelle etc. (in parts
  4411 still somewhat experimental); old Makefiles etc. still functional;
  4412 
  4413 * new 'Isabelle System Manual';
  4414 
  4415 * INSTALL text, together with ./configure and ./build scripts;
  4416 
  4417 * reimplemented type inference for greater efficiency, better error
  4418 messages and clean internal interface;
  4419 
  4420 * prlim command for dealing with lots of subgoals (an easier way of
  4421 setting goals_limit);
  4422 
  4423 
  4424 *** Syntax ***
  4425 
  4426 * supports alternative (named) syntax tables (parser and pretty
  4427 printer); internal interface is provided by add_modesyntax(_i);
  4428 
  4429 * Pure, FOL, ZF, HOL, HOLCF now support symbolic input and output; to
  4430 be used in conjunction with the Isabelle symbol font; uses the
  4431 "symbols" syntax table;
  4432 
  4433 * added token_translation interface (may translate name tokens in
  4434 arbitrary ways, dependent on their type (free, bound, tfree, ...) and
  4435 the current print_mode); IMPORTANT: user print translation functions
  4436 are responsible for marking newly introduced bounds
  4437 (Syntax.mark_boundT);
  4438 
  4439 * token translations for modes "xterm" and "xterm_color" that display
  4440 names in bold, underline etc. or colors (which requires a color
  4441 version of xterm);
  4442 
  4443 * infixes may now be declared with names independent of their syntax;
  4444 
  4445 * added typed_print_translation (like print_translation, but may
  4446 access type of constant);
  4447 
  4448 
  4449 *** Classical Reasoner ***
  4450 
  4451 Blast_tac: a new tactic!  It is often more powerful than fast_tac, but has
  4452 some limitations.  Blast_tac...
  4453   + ignores addss, addbefore, addafter; this restriction is intrinsic
  4454   + ignores elimination rules that don't have the correct format
  4455         (the conclusion MUST be a formula variable)
  4456   + ignores types, which can make HOL proofs fail
  4457   + rules must not require higher-order unification, e.g. apply_type in ZF
  4458     [message "Function Var's argument not a bound variable" relates to this]
  4459   + its proof strategy is more general but can actually be slower
  4460 
  4461 * substitution with equality assumptions no longer permutes other
  4462 assumptions;
  4463 
  4464 * minor changes in semantics of addafter (now called addaltern); renamed
  4465 setwrapper to setWrapper and compwrapper to compWrapper; added safe wrapper
  4466 (and access functions for it);
  4467 
  4468 * improved combination of classical reasoner and simplifier:
  4469   + functions for handling clasimpsets
  4470   + improvement of addss: now the simplifier is called _after_ the
  4471     safe steps.
  4472   + safe variant of addss called addSss: uses safe simplifications
  4473     _during_ the safe steps. It is more complete as it allows multiple
  4474     instantiations of unknowns (e.g. with slow_tac).
  4475 
  4476 *** Simplifier ***
  4477 
  4478 * added interface for simplification procedures (functions that
  4479 produce *proven* rewrite rules on the fly, depending on current
  4480 redex);
  4481 
  4482 * ordering on terms as parameter (used for ordered rewriting);
  4483 
  4484 * new functions delcongs, deleqcongs, and Delcongs. richer rep_ss;
  4485 
  4486 * the solver is now split into a safe and an unsafe part.
  4487 This should be invisible for the normal user, except that the
  4488 functions setsolver and addsolver have been renamed to setSolver and
  4489 addSolver; added safe_asm_full_simp_tac;
  4490 
  4491 
  4492 *** HOL ***
  4493 
  4494 * a generic induction tactic `induct_tac' which works for all datatypes and
  4495 also for type `nat';
  4496 
  4497 * a generic case distinction tactic `exhaust_tac' which works for all
  4498 datatypes and also for type `nat';
  4499 
  4500 * each datatype comes with a function `size';
  4501 
  4502 * patterns in case expressions allow tuple patterns as arguments to
  4503 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';
  4504 
  4505 * primrec now also works with type nat;
  4506 
  4507 * recdef: a new declaration form, allows general recursive functions to be
  4508 defined in theory files.  See HOL/ex/Fib, HOL/ex/Primes, HOL/Subst/Unify.
  4509 
  4510 * the constant for negation has been renamed from "not" to "Not" to
  4511 harmonize with FOL, ZF, LK, etc.;
  4512 
  4513 * HOL/ex/LFilter theory of a corecursive "filter" functional for
  4514 infinite lists;
  4515 
  4516 * HOL/Modelcheck demonstrates invocation of model checker oracle;
  4517 
  4518 * HOL/ex/Ring.thy declares cring_simp, which solves equational
  4519 problems in commutative rings, using axiomatic type classes for + and *;
  4520 
  4521 * more examples in HOL/MiniML and HOL/Auth;
  4522 
  4523 * more default rewrite rules for quantifiers, union/intersection;
  4524 
  4525 * a new constant `arbitrary == @x.False';
  4526 
  4527 * HOLCF/IOA replaces old HOL/IOA;
  4528 
  4529 * HOLCF changes: derived all rules and arities
  4530   + axiomatic type classes instead of classes
  4531   + typedef instead of faking type definitions
  4532   + eliminated the internal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
  4533   + new axclasses cpo, chfin, flat with flat < chfin < pcpo < cpo < po
  4534   + eliminated the types void, one, tr
  4535   + use unit lift and bool lift (with translations) instead of one and tr
  4536   + eliminated blift from Lift3.thy (use Def instead of blift)
  4537   all eliminated rules are derived as theorems --> no visible changes ;
  4538 
  4539 
  4540 *** ZF ***
  4541 
  4542 * ZF now has Fast_tac, Simp_tac and Auto_tac.  Union_iff is a now a default
  4543 rewrite rule; this may affect some proofs.  eq_cs is gone but can be put back
  4544 as ZF_cs addSIs [equalityI];
  4545 
  4546 
  4547 
  4548 New in Isabelle94-7 (November 96)
  4549 ---------------------------------
  4550 
  4551 * allowing negative levels (as offsets) in prlev and choplev;
  4552 
  4553 * super-linear speedup for large simplifications;
  4554 
  4555 * FOL, ZF and HOL now use miniscoping: rewriting pushes
  4556 quantifications in as far as possible (COULD MAKE EXISTING PROOFS
  4557 FAIL); can suppress it using the command Delsimps (ex_simps @
  4558 all_simps); De Morgan laws are also now included, by default;
  4559 
  4560 * improved printing of ==>  :  ~:
  4561 
  4562 * new object-logic "Sequents" adds linear logic, while replacing LK
  4563 and Modal (thanks to Sara Kalvala);
  4564 
  4565 * HOL/Auth: correctness proofs for authentication protocols;
  4566 
  4567 * HOL: new auto_tac combines rewriting and classical reasoning (many
  4568 examples on HOL/Auth);
  4569 
  4570 * HOL: new command AddIffs for declaring theorems of the form P=Q to
  4571 the rewriter and classical reasoner simultaneously;
  4572 
  4573 * function uresult no longer returns theorems in "standard" format;
  4574 regain previous version by: val uresult = standard o uresult;
  4575 
  4576 
  4577 
  4578 New in Isabelle94-6
  4579 -------------------
  4580 
  4581 * oracles -- these establish an interface between Isabelle and trusted
  4582 external reasoners, which may deliver results as theorems;
  4583 
  4584 * proof objects (in particular record all uses of oracles);
  4585 
  4586 * Simp_tac, Fast_tac, etc. that refer to implicit simpset / claset;
  4587 
  4588 * "constdefs" section in theory files;
  4589 
  4590 * "primrec" section (HOL) no longer requires names;
  4591 
  4592 * internal type "tactic" now simply "thm -> thm Sequence.seq";
  4593 
  4594 
  4595 
  4596 New in Isabelle94-5
  4597 -------------------
  4598 
  4599 * reduced space requirements;
  4600 
  4601 * automatic HTML generation from theories;
  4602 
  4603 * theory files no longer require "..." (quotes) around most types;
  4604 
  4605 * new examples, including two proofs of the Church-Rosser theorem;
  4606 
  4607 * non-curried (1994) version of HOL is no longer distributed;
  4608 
  4609 
  4610 
  4611 New in Isabelle94-4
  4612 -------------------
  4613 
  4614 * greatly reduced space requirements;
  4615 
  4616 * theory files (.thy) no longer require \...\ escapes at line breaks;
  4617 
  4618 * searchable theorem database (see the section "Retrieving theorems" on
  4619 page 8 of the Reference Manual);
  4620 
  4621 * new examples, including Grabczewski's monumental case study of the
  4622 Axiom of Choice;
  4623 
  4624 * The previous version of HOL renamed to Old_HOL;
  4625 
  4626 * The new version of HOL (previously called CHOL) uses a curried syntax
  4627 for functions.  Application looks like f a b instead of f(a,b);
  4628 
  4629 * Mutually recursive inductive definitions finally work in HOL;
  4630 
  4631 * In ZF, pattern-matching on tuples is now available in all abstractions and
  4632 translates to the operator "split";
  4633 
  4634 
  4635 
  4636 New in Isabelle94-3
  4637 -------------------
  4638 
  4639 * new infix operator, addss, allowing the classical reasoner to
  4640 perform simplification at each step of its search.  Example:
  4641         fast_tac (cs addss ss)
  4642 
  4643 * a new logic, CHOL, the same as HOL, but with a curried syntax
  4644 for functions.  Application looks like f a b instead of f(a,b).  Also pairs
  4645 look like (a,b) instead of <a,b>;
  4646 
  4647 * PLEASE NOTE: CHOL will eventually replace HOL!
  4648 
  4649 * In CHOL, pattern-matching on tuples is now available in all abstractions.
  4650 It translates to the operator "split".  A new theory of integers is available;
  4651 
  4652 * In ZF, integer numerals now denote two's-complement binary integers.
  4653 Arithmetic operations can be performed by rewriting.  See ZF/ex/Bin.ML;
  4654 
  4655 * Many new examples: I/O automata, Church-Rosser theorem, equivalents
  4656 of the Axiom of Choice;
  4657 
  4658 
  4659 
  4660 New in Isabelle94-2
  4661 -------------------
  4662 
  4663 * Significantly faster resolution;
  4664 
  4665 * the different sections in a .thy file can now be mixed and repeated
  4666 freely;
  4667 
  4668 * Database of theorems for FOL, HOL and ZF.  New
  4669 commands including qed, qed_goal and bind_thm store theorems in the database.
  4670 
  4671 * Simple database queries: return a named theorem (get_thm) or all theorems of
  4672 a given theory (thms_of), or find out what theory a theorem was proved in
  4673 (theory_of_thm);
  4674 
  4675 * Bugs fixed in the inductive definition and datatype packages;
  4676 
  4677 * The classical reasoner provides deepen_tac and depth_tac, making FOL_dup_cs
  4678 and HOL_dup_cs obsolete;
  4679 
  4680 * Syntactic ambiguities caused by the new treatment of syntax in Isabelle94-1
  4681 have been removed;
  4682 
  4683 * Simpler definition of function space in ZF;
  4684 
  4685 * new results about cardinal and ordinal arithmetic in ZF;
  4686 
  4687 * 'subtype' facility in HOL for introducing new types as subsets of existing
  4688 types;
  4689 
  4690 
  4691 $Id$