NEWS
 author hoelzl Tue Nov 05 09:45:03 2013 +0100 (2013-11-05) changeset 54264 27501a51d847 parent 54250 7d2544dd3988 child 54295 45a5523d4a63 permissions -rw-r--r--
NEWS
 wenzelm@5363 ` 1` ```Isabelle NEWS -- history user-relevant changes ``` wenzelm@5363 ` 2` ```============================================== ``` wenzelm@2553 ` 3` wenzelm@54055 ` 4` ```New in this Isabelle version ``` wenzelm@54055 ` 5` ```---------------------------- ``` wenzelm@54055 ` 6` haftmann@54227 ` 7` ```*** HOL *** ``` haftmann@54227 ` 8` haftmann@54228 ` 9` ```* Fact generalization and consolidation: ``` haftmann@54228 ` 10` ``` neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 ``` haftmann@54228 ` 11` ```INCOMPATIBILITY. ``` haftmann@54228 ` 12` haftmann@54228 ` 13` ```* Purely algebraic definition of even. Fact generalization and consolidation: ``` haftmann@54228 ` 14` ``` nat_even_iff_2_dvd, int_even_iff_2_dvd ~> even_iff_2_dvd ``` haftmann@54228 ` 15` ``` even_zero_(nat|int) ~> even_zero ``` haftmann@54228 ` 16` ```INCOMPATIBILITY. ``` wenzelm@54055 ` 17` haftmann@54230 ` 18` ```* Elimination of fact duplicates: ``` haftmann@54230 ` 19` ``` equals_zero_I ~> minus_unique ``` haftmann@54230 ` 20` ``` diff_eq_0_iff_eq ~> right_minus_eq ``` haftmann@54230 ` 21` ```INCOMPATIBILITY. ``` haftmann@54230 ` 22` haftmann@54230 ` 23` ```* Fact name consolidation: ``` haftmann@54230 ` 24` ``` diff_def, diff_minus, ab_diff_minus ~> diff_conv_add_uminus ``` haftmann@54250 ` 25` ``` minus_le_self_iff ~> neg_less_eq_nonneg ``` haftmann@54250 ` 26` ``` le_minus_self_iff ~> less_eq_neg_nonpos ``` haftmann@54250 ` 27` ``` neg_less_nonneg ~> neg_less_pos ``` haftmann@54250 ` 28` ``` less_minus_self_iff ~> less_neg_neg [simp] ``` haftmann@54230 ` 29` ```INCOMPATIBILITY. ``` haftmann@54230 ` 30` haftmann@54230 ` 31` ```* More simplification rules on unary and binary minus: ``` haftmann@54230 ` 32` ```add_diff_cancel, add_diff_cancel_left, add_le_same_cancel1, ``` haftmann@54230 ` 33` ```add_le_same_cancel2, add_less_same_cancel1, add_less_same_cancel2, ``` haftmann@54230 ` 34` ```add_minus_cancel, diff_add_cancel, le_add_same_cancel1, ``` haftmann@54230 ` 35` ```le_add_same_cancel2, less_add_same_cancel1, less_add_same_cancel2, ``` haftmann@54230 ` 36` ```minus_add_cancel, uminus_add_conv_diff. These correspondingly ``` haftmann@54230 ` 37` ```have been taken away from fact collections algebra_simps and ``` haftmann@54230 ` 38` ```field_simps. INCOMPATIBILITY. ``` haftmann@54230 ` 39` haftmann@54230 ` 40` ```To restore proofs, the following patterns are helpful: ``` haftmann@54230 ` 41` haftmann@54230 ` 42` ```a) Arbitrary failing proof not involving "diff_def": ``` haftmann@54230 ` 43` ```Consider simplification with algebra_simps or field_simps. ``` haftmann@54230 ` 44` haftmann@54230 ` 45` ```b) Lifting rules from addition to subtraction: ``` haftmann@54230 ` 46` ```Try with "using of [… "- _" …]" by simp". ``` haftmann@54230 ` 47` haftmann@54230 ` 48` ```c) Simplification with "diff_def": just drop "diff_def". ``` haftmann@54230 ` 49` ```Consider simplification with algebra_simps or field_simps; ``` haftmann@54230 ` 50` ```or the brute way with ``` haftmann@54230 ` 51` ```"simp add: diff_conv_add_uminus del: add_uminus_conv_diff". ``` haftmann@54230 ` 52` hoelzl@54264 ` 53` ```* SUP and INF generalized to conditionally_complete_lattice ``` hoelzl@54264 ` 54` hoelzl@54264 ` 55` ```* Theory Lubs moved HOL image to HOL-Library. It is replaced by ``` hoelzl@54264 ` 56` ```Conditionally_Complete_Lattices. INCOMPATIBILITY. ``` hoelzl@54264 ` 57` hoelzl@54264 ` 58` ```* Introduce bdd_above and bdd_below in Conditionally_Complete_Lattices, use them ``` hoelzl@54264 ` 59` ```instead of explicitly stating boundedness of sets. ``` hoelzl@54264 ` 60` hoelzl@54264 ` 61` wenzelm@53971 ` 62` ```New in Isabelle2013-1 (November 2013) ``` wenzelm@53971 ` 63` ```------------------------------------- ``` wenzelm@50994 ` 64` wenzelm@51293 ` 65` ```*** General *** ``` wenzelm@51293 ` 66` wenzelm@53971 ` 67` ```* Discontinued obsolete 'uses' within theory header. Note that ``` wenzelm@53971 ` 68` ```commands like 'ML_file' work without separate declaration of file ``` wenzelm@53971 ` 69` ```dependencies. Minor INCOMPATIBILITY. ``` wenzelm@53971 ` 70` wenzelm@53971 ` 71` ```* Discontinued redundant 'use' command, which was superseded by ``` wenzelm@53971 ` 72` ```'ML_file' in Isabelle2013. Minor INCOMPATIBILITY. ``` wenzelm@53971 ` 73` wenzelm@53016 ` 74` ```* Simplified subscripts within identifiers, using plain \<^sub> ``` wenzelm@53016 ` 75` ```instead of the second copy \<^isub> and \<^isup>. Superscripts are ``` wenzelm@53016 ` 76` ```only for literal tokens within notation; explicit mixfix annotations ``` wenzelm@53016 ` 77` ```for consts or fixed variables may be used as fall-back for unusual ``` wenzelm@53016 ` 78` ```names. Obsolete \ has been expanded to \<^sup>2 in ``` wenzelm@53016 ` 79` ```Isabelle/HOL. INCOMPATIBILITY, use "isabelle update_sub_sup" to ``` wenzelm@53016 ` 80` ```standardize symbols as a starting point for further manual cleanup. ``` wenzelm@53016 ` 81` ```The ML reference variable "legacy_isub_isup" may be set as temporary ``` wenzelm@53016 ` 82` ```workaround, to make the prover accept a subset of the old identifier ``` wenzelm@53016 ` 83` ```syntax. ``` wenzelm@53016 ` 84` wenzelm@53021 ` 85` ```* Document antiquotations: term style "isub" has been renamed to ``` wenzelm@53021 ` 86` ```"sub". Minor INCOMPATIBILITY. ``` wenzelm@53021 ` 87` wenzelm@52487 ` 88` ```* Uniform management of "quick_and_dirty" as system option (see also ``` wenzelm@52487 ` 89` ```"isabelle options"), configuration option within the context (see also ``` wenzelm@52487 ` 90` ```Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor ``` wenzelm@52487 ` 91` ```INCOMPATIBILITY, need to use more official Isabelle means to access ``` wenzelm@52487 ` 92` ```quick_and_dirty, instead of historical poking into mutable reference. ``` wenzelm@52059 ` 93` wenzelm@52060 ` 94` ```* Renamed command 'print_configs' to 'print_options'. Minor ``` wenzelm@52060 ` 95` ```INCOMPATIBILITY. ``` wenzelm@52060 ` 96` wenzelm@52430 ` 97` ```* Proper diagnostic command 'print_state'. Old 'pr' (with its ``` wenzelm@52430 ` 98` ```implicit change of some global references) is retained for now as ``` wenzelm@52430 ` 99` ```control command, e.g. for ProofGeneral 3.7.x. ``` wenzelm@52430 ` 100` wenzelm@52549 ` 101` ```* Discontinued 'print_drafts' command with its old-fashioned PS output ``` wenzelm@52549 ` 102` ```and Unix command-line print spooling. Minor INCOMPATIBILITY: use ``` wenzelm@52549 ` 103` ```'display_drafts' instead and print via the regular document viewer. ``` wenzelm@52549 ` 104` wenzelm@53971 ` 105` ```* Updated and extended "isar-ref" and "implementation" manual, ``` wenzelm@53971 ` 106` ```eliminated old "ref" manual. ``` wenzelm@53971 ` 107` wenzelm@51293 ` 108` wenzelm@51533 ` 109` ```*** Prover IDE -- Isabelle/Scala/jEdit *** ``` wenzelm@51533 ` 110` wenzelm@53971 ` 111` ```* New manual "jedit" for Isabelle/jEdit, see isabelle doc or ``` wenzelm@53852 ` 112` ```Documentation panel. ``` wenzelm@53852 ` 113` wenzelm@53971 ` 114` ```* Dockable window "Documentation" provides access to Isabelle ``` wenzelm@53971 ` 115` ```documentation. ``` wenzelm@52646 ` 116` wenzelm@52949 ` 117` ```* Dockable window "Find" provides query operations for formal entities ``` wenzelm@52949 ` 118` ```(GUI front-end to 'find_theorems' command). ``` wenzelm@52949 ` 119` wenzelm@53050 ` 120` ```* Dockable window "Sledgehammer" manages asynchronous / parallel ``` wenzelm@53050 ` 121` ```sledgehammer runs over existing document sources, independently of ``` wenzelm@53050 ` 122` ```normal editing and checking process. ``` wenzelm@53050 ` 123` wenzelm@51533 ` 124` ```* Dockable window "Timing" provides an overview of relevant command ``` wenzelm@51533 ` 125` ```timing information. ``` wenzelm@51533 ` 126` wenzelm@53971 ` 127` ```* Improved dockable window "Theories": Continuous checking of proof ``` wenzelm@53971 ` 128` ```document (visible and required parts) may be controlled explicitly, ``` wenzelm@53971 ` 129` ```using check box or shortcut "C+e ENTER". Individual theory nodes may ``` wenzelm@53971 ` 130` ```be marked explicitly as required and checked in full, using check box ``` wenzelm@53971 ` 131` ```or shortcut "C+e SPACE". ``` wenzelm@53971 ` 132` wenzelm@53971 ` 133` ```* Strictly monotonic document update, without premature cancellation of ``` wenzelm@53971 ` 134` ```running transactions that are still needed: avoid reset/restart of ``` wenzelm@53971 ` 135` ```such command executions while editing. ``` wenzelm@53271 ` 136` wenzelm@53326 ` 137` ```* Improved completion mechanism, which is now managed by the ``` wenzelm@53981 ` 138` ```Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle ``` wenzelm@53981 ` 139` ```symbol abbreviations (see \$ISABELLE_HOME/etc/symbols). ``` wenzelm@53326 ` 140` wenzelm@53971 ` 141` ```* Support for asynchronous print functions, as overlay to existing ``` wenzelm@53971 ` 142` ```document content. ``` wenzelm@53971 ` 143` wenzelm@53971 ` 144` ```* Support for automatic tools in HOL, which try to prove or disprove ``` wenzelm@53971 ` 145` ```toplevel theorem statements. ``` wenzelm@53971 ` 146` wenzelm@53971 ` 147` ```* Action isabelle.reset-font-size resets main text area font size ``` wenzelm@53971 ` 148` ```according to Isabelle/Scala plugin option "jedit_font_reset_size" ``` wenzelm@53971 ` 149` ```(cf. keyboard shortcut C+0). ``` wenzelm@53971 ` 150` wenzelm@53971 ` 151` ```* File specifications in jEdit (e.g. file browser) may refer to ``` wenzelm@53971 ` 152` ```\$ISABELLE_HOME on all platforms. Discontinued obsolete ``` wenzelm@53971 ` 153` ```\$ISABELLE_HOME_WINDOWS variable. ``` wenzelm@53971 ` 154` wenzelm@53971 ` 155` ```* Improved support for Linux look-and-feel "GTK+", see also "Utilities ``` wenzelm@53971 ` 156` ```/ Global Options / Appearance". ``` wenzelm@53971 ` 157` wenzelm@53971 ` 158` ```* Improved support of native Mac OS X functionality via "MacOSX" ``` wenzelm@53971 ` 159` ```plugin, which is now enabled by default. ``` wenzelm@53971 ` 160` wenzelm@51533 ` 161` wenzelm@51313 ` 162` ```*** Pure *** ``` wenzelm@51313 ` 163` ballarin@54049 ` 164` ```* Commands 'interpretation' and 'sublocale' are now target-sensitive. ``` ballarin@54049 ` 165` ```In particular, 'interpretation' allows for non-persistent ``` ballarin@54049 ` 166` ```interpretation within "context ... begin ... end" blocks offering a ``` ballarin@54049 ` 167` ```light-weight alternative to 'sublocale'. See "isar-ref" manual for ``` ballarin@54049 ` 168` ```details. ``` haftmann@51747 ` 169` ballarin@51565 ` 170` ```* Improved locales diagnostic command 'print_dependencies'. ``` ballarin@51565 ` 171` wenzelm@51313 ` 172` ```* Discontinued obsolete 'axioms' command, which has been marked as ``` wenzelm@51313 ` 173` ```legacy since Isabelle2009-2. INCOMPATIBILITY, use 'axiomatization' ``` wenzelm@51313 ` 174` ```instead, while observing its uniform scope for polymorphism. ``` wenzelm@51313 ` 175` wenzelm@51316 ` 176` ```* Discontinued empty name bindings in 'axiomatization'. ``` wenzelm@51316 ` 177` ```INCOMPATIBILITY. ``` wenzelm@51316 ` 178` wenzelm@53971 ` 179` ```* System option "proofs" has been discontinued. Instead the global ``` wenzelm@53971 ` 180` ```state of Proofterm.proofs is persistently compiled into logic images ``` wenzelm@53971 ` 181` ```as required, notably HOL-Proofs. Users no longer need to change ``` wenzelm@53971 ` 182` ```Proofterm.proofs dynamically. Minor INCOMPATIBILITY. ``` wenzelm@53971 ` 183` wenzelm@53971 ` 184` ```* Syntax translation functions (print_translation etc.) always depend ``` wenzelm@53971 ` 185` ```on Proof.context. Discontinued former "(advanced)" option -- this is ``` wenzelm@53971 ` 186` ```now the default. Minor INCOMPATIBILITY. ``` wenzelm@53971 ` 187` wenzelm@53971 ` 188` ```* Former global reference trace_unify_fail is now available as ``` wenzelm@53971 ` 189` ```configuration option "unify_trace_failure" (global context only). ``` wenzelm@53971 ` 190` wenzelm@52463 ` 191` ```* SELECT_GOAL now retains the syntactic context of the overall goal ``` wenzelm@52463 ` 192` ```state (schematic variables etc.). Potential INCOMPATIBILITY in rare ``` wenzelm@52463 ` 193` ```situations. ``` wenzelm@52463 ` 194` wenzelm@51313 ` 195` hoelzl@51002 ` 196` ```*** HOL *** ``` hoelzl@51002 ` 197` wenzelm@54032 ` 198` ```* Stronger precedence of syntax for big intersection and union on ``` wenzelm@54032 ` 199` ```sets, in accordance with corresponding lattice operations. ``` wenzelm@54032 ` 200` ```INCOMPATIBILITY. ``` wenzelm@54032 ` 201` wenzelm@54032 ` 202` ```* Notation "{p:A. P}" now allows tuple patterns as well. ``` wenzelm@54032 ` 203` wenzelm@54032 ` 204` ```* Nested case expressions are now translated in a separate check phase ``` wenzelm@54032 ` 205` ```rather than during parsing. The data for case combinators is separated ``` wenzelm@54032 ` 206` ```from the datatype package. The declaration attribute ``` wenzelm@54032 ` 207` ```"case_translation" can be used to register new case combinators: ``` wenzelm@54032 ` 208` wenzelm@54032 ` 209` ``` declare [[case_translation case_combinator constructor1 ... constructorN]] ``` haftmann@52637 ` 210` haftmann@52435 ` 211` ```* Code generator: ``` wenzelm@53160 ` 212` ``` - 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / ``` wenzelm@53160 ` 213` ``` 'code_instance'. ``` wenzelm@53160 ` 214` ``` - 'code_identifier' declares name hints for arbitrary identifiers in ``` wenzelm@53160 ` 215` ``` generated code, subsuming 'code_modulename'. ``` wenzelm@53983 ` 216` wenzelm@53983 ` 217` ```See the isar-ref manual for syntax diagrams, and the HOL theories for ``` wenzelm@53983 ` 218` ```examples. ``` haftmann@52435 ` 219` wenzelm@54032 ` 220` ```* Attibute 'code': 'code' now declares concrete and abstract code ``` wenzelm@54032 ` 221` ```equations uniformly. Use explicit 'code equation' and 'code abstract' ``` wenzelm@54032 ` 222` ```to distinguish both when desired. ``` wenzelm@54032 ` 223` wenzelm@54032 ` 224` ```* Discontinued theories Code_Integer and Efficient_Nat by a more ``` wenzelm@54032 ` 225` ```fine-grain stack of theories Code_Target_Int, Code_Binary_Nat, ``` wenzelm@54032 ` 226` ```Code_Target_Nat and Code_Target_Numeral. See the tutorial on code ``` wenzelm@54032 ` 227` ```generation for details. INCOMPATIBILITY. ``` wenzelm@54032 ` 228` wenzelm@54032 ` 229` ```* Numeric types are mapped by default to target language numerals: ``` wenzelm@54032 ` 230` ```natural (replaces former code_numeral) and integer (replaces former ``` wenzelm@54032 ` 231` ```code_int). Conversions are available as integer_of_natural / ``` wenzelm@54032 ` 232` ```natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and ``` wenzelm@54032 ` 233` ```Code_Numeral.integer_of_natural / Code_Numeral.natural_of_integer (in ``` wenzelm@54032 ` 234` ```ML). INCOMPATIBILITY. ``` wenzelm@54032 ` 235` wenzelm@54032 ` 236` ```* Function package: For mutually recursive functions f and g, separate ``` wenzelm@54032 ` 237` ```cases rules f.cases and g.cases are generated instead of unusable ``` wenzelm@54032 ` 238` ```f_g.cases which exposed internal sum types. Potential INCOMPATIBILITY, ``` wenzelm@54032 ` 239` ```in the case that the unusable rule was used nevertheless. ``` wenzelm@54032 ` 240` wenzelm@54032 ` 241` ```* Function package: For each function f, new rules f.elims are ``` wenzelm@54032 ` 242` ```generated, which eliminate equalities of the form "f x = t". ``` wenzelm@54032 ` 243` wenzelm@54032 ` 244` ```* New command 'fun_cases' derives ad-hoc elimination rules for ``` wenzelm@54032 ` 245` ```function equations as simplified instances of f.elims, analogous to ``` wenzelm@54032 ` 246` ```inductive_cases. See ~~/src/HOL/ex/Fundefs.thy for some examples. ``` blanchet@53307 ` 247` kuncar@54021 ` 248` ```* Lifting: ``` kuncar@54021 ` 249` ``` - parametrized correspondence relations are now supported: ``` kuncar@54021 ` 250` ``` + parametricity theorems for the raw term can be specified in ``` kuncar@54021 ` 251` ``` the command lift_definition, which allow us to generate stronger ``` kuncar@54021 ` 252` ``` transfer rules ``` kuncar@54021 ` 253` ``` + setup_lifting generates stronger transfer rules if parametric ``` kuncar@54021 ` 254` ``` correspondence relation can be generated ``` kuncar@54021 ` 255` ``` + various new properties of the relator must be specified to support ``` kuncar@54021 ` 256` ``` parametricity ``` kuncar@54021 ` 257` ``` + parametricity theorem for the Quotient relation can be specified ``` kuncar@54021 ` 258` ``` - setup_lifting generates domain rules for the Transfer package ``` kuncar@54021 ` 259` ``` - stronger reflexivity prover of respectfulness theorems for type ``` kuncar@54021 ` 260` ``` copies ``` kuncar@54021 ` 261` ``` - ===> and --> are now local. The symbols can be introduced ``` kuncar@54021 ` 262` ``` by interpreting the locale lifting_syntax (typically in an ``` kuncar@54021 ` 263` ``` anonymous context) ``` kuncar@54021 ` 264` ``` - Lifting/Transfer relevant parts of Library/Quotient_* are now in ``` kuncar@54021 ` 265` ``` Main. Potential INCOMPATIBILITY ``` kuncar@54021 ` 266` ``` - new commands for restoring and deleting Lifting/Transfer context: ``` kuncar@54021 ` 267` ``` lifting_forget, lifting_update ``` kuncar@54021 ` 268` ``` - the command print_quotmaps was renamed to print_quot_maps. ``` kuncar@54021 ` 269` ``` INCOMPATIBILITY ``` kuncar@54021 ` 270` kuncar@54021 ` 271` ```* Transfer: ``` kuncar@54021 ` 272` ``` - better support for domains in Transfer: replace Domainp T ``` kuncar@54021 ` 273` ``` by the actual invariant in a transferred goal ``` kuncar@54021 ` 274` ``` - transfer rules can have as assumptions other transfer rules ``` kuncar@54021 ` 275` ``` - Experimental support for transferring from the raw level to the ``` kuncar@54021 ` 276` ``` abstract level: Transfer.transferred attribute ``` kuncar@54021 ` 277` ``` - Attribute version of the transfer method: untransferred attribute ``` kuncar@54021 ` 278` haftmann@52286 ` 279` ```* Reification and reflection: ``` wenzelm@53160 ` 280` ``` - Reification is now directly available in HOL-Main in structure ``` wenzelm@53160 ` 281` ``` "Reification". ``` wenzelm@53160 ` 282` ``` - Reflection now handles multiple lists with variables also. ``` wenzelm@53160 ` 283` ``` - The whole reflection stack has been decomposed into conversions. ``` haftmann@52286 ` 284` ```INCOMPATIBILITY. ``` haftmann@52286 ` 285` haftmann@51489 ` 286` ```* Revised devices for recursive definitions over finite sets: ``` haftmann@51489 ` 287` ``` - Only one fundamental fold combinator on finite set remains: ``` haftmann@51489 ` 288` ``` Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b ``` haftmann@51489 ` 289` ``` This is now identity on infinite sets. ``` wenzelm@52745 ` 290` ``` - Locales ("mini packages") for fundamental definitions with ``` haftmann@51489 ` 291` ``` Finite_Set.fold: folding, folding_idem. ``` haftmann@51489 ` 292` ``` - Locales comm_monoid_set, semilattice_order_set and ``` haftmann@51489 ` 293` ``` semilattice_neutr_order_set for big operators on sets. ``` haftmann@51489 ` 294` ``` See theory Big_Operators for canonical examples. ``` haftmann@51489 ` 295` ``` Note that foundational constants comm_monoid_set.F and ``` haftmann@51489 ` 296` ``` semilattice_set.F correspond to former combinators fold_image ``` haftmann@51489 ` 297` ``` and fold1 respectively. These are now gone. You may use ``` haftmann@51490 ` 298` ``` those foundational constants as substitutes, but it is ``` wenzelm@53983 ` 299` ``` preferable to interpret the above locales accordingly. ``` haftmann@51489 ` 300` ``` - Dropped class ab_semigroup_idem_mult (special case of lattice, ``` haftmann@51489 ` 301` ``` no longer needed in connection with Finite_Set.fold etc.) ``` haftmann@51489 ` 302` ``` - Fact renames: ``` haftmann@51489 ` 303` ``` card.union_inter ~> card_Un_Int [symmetric] ``` haftmann@51489 ` 304` ``` card.union_disjoint ~> card_Un_disjoint ``` haftmann@51489 ` 305` ```INCOMPATIBILITY. ``` haftmann@51489 ` 306` haftmann@51487 ` 307` ```* Locale hierarchy for abstract orderings and (semi)lattices. ``` haftmann@51487 ` 308` wenzelm@53526 ` 309` ```* Complete_Partial_Order.admissible is defined outside the type class ``` wenzelm@53526 ` 310` ```ccpo, but with mandatory prefix ccpo. Admissibility theorems lose the ``` wenzelm@53526 ` 311` ```class predicate assumption or sort constraint when possible. ``` Andreas@53362 ` 312` ```INCOMPATIBILITY. ``` Andreas@53362 ` 313` wenzelm@53160 ` 314` ```* Introduce type class "conditionally_complete_lattice": Like a ``` wenzelm@53160 ` 315` ```complete lattice but does not assume the existence of the top and ``` wenzelm@53160 ` 316` ```bottom elements. Allows to generalize some lemmas about reals and ``` wenzelm@53160 ` 317` ```extended reals. Removed SupInf and replaced it by the instantiation ``` wenzelm@53160 ` 318` ```of conditionally_complete_lattice for real. Renamed lemmas about ``` wenzelm@53160 ` 319` ```conditionally-complete lattice from Sup_... to cSup_... and from ``` wenzelm@53160 ` 320` ```Inf_... to cInf_... to avoid hidding of similar complete lattice ``` wenzelm@53160 ` 321` ```lemmas. ``` wenzelm@53160 ` 322` wenzelm@53160 ` 323` ```* Introduce type class linear_continuum as combination of ``` wenzelm@53160 ` 324` ```conditionally-complete lattices and inner dense linorders which have ``` wenzelm@53160 ` 325` ```more than one element. INCOMPATIBILITY. ``` wenzelm@53160 ` 326` wenzelm@53983 ` 327` ```* Introduced type classes order_top and order_bot. The old classes top ``` wenzelm@53983 ` 328` ```and bot only contain the syntax without assumptions. INCOMPATIBILITY: ``` wenzelm@53983 ` 329` ```Rename bot -> order_bot, top -> order_top ``` lammich@53683 ` 330` wenzelm@53160 ` 331` ```* Introduce type classes "no_top" and "no_bot" for orderings without ``` wenzelm@53160 ` 332` ```top and bottom elements. ``` hoelzl@51732 ` 333` hoelzl@51732 ` 334` ```* Split dense_linorder into inner_dense_order and no_top, no_bot. ``` hoelzl@51732 ` 335` hoelzl@51732 ` 336` ```* Complex_Main: Unify and move various concepts from ``` wenzelm@53160 ` 337` ```HOL-Multivariate_Analysis to HOL-Complex_Main. ``` hoelzl@51732 ` 338` wenzelm@53983 ` 339` ``` - Introduce type class (lin)order_topology and ``` wenzelm@53983 ` 340` ``` linear_continuum_topology. Allows to generalize theorems about ``` wenzelm@53983 ` 341` ``` limits and order. Instances are reals and extended reals. ``` hoelzl@51732 ` 342` hoelzl@51732 ` 343` ``` - continuous and continuos_on from Multivariate_Analysis: ``` wenzelm@53983 ` 344` ``` "continuous" is the continuity of a function at a filter. "isCont" ``` wenzelm@53983 ` 345` ``` is now an abbrevitation: "isCont x f == continuous (at _) f". ``` wenzelm@53983 ` 346` wenzelm@53983 ` 347` ``` Generalized continuity lemmas from isCont to continuous on an ``` wenzelm@53983 ` 348` ``` arbitrary filter. ``` wenzelm@53983 ` 349` wenzelm@53983 ` 350` ``` - compact from Multivariate_Analysis. Use Bolzano's lemma to prove ``` wenzelm@53983 ` 351` ``` compactness of closed intervals on reals. Continuous functions ``` wenzelm@53983 ` 352` ``` attain infimum and supremum on compact sets. The inverse of a ``` wenzelm@53983 ` 353` ``` continuous function is continuous, when the function is continuous ``` wenzelm@53983 ` 354` ``` on a compact set. ``` hoelzl@51732 ` 355` hoelzl@51732 ` 356` ``` - connected from Multivariate_Analysis. Use it to prove the ``` hoelzl@51775 ` 357` ``` intermediate value theorem. Show connectedness of intervals on ``` hoelzl@51775 ` 358` ``` linear_continuum_topology). ``` hoelzl@51732 ` 359` hoelzl@51732 ` 360` ``` - first_countable_topology from Multivariate_Analysis. Is used to ``` wenzelm@53983 ` 361` ``` show equivalence of properties on the neighbourhood filter of x and ``` wenzelm@53983 ` 362` ``` on all sequences converging to x. ``` wenzelm@53983 ` 363` wenzelm@53983 ` 364` ``` - FDERIV: Definition of has_derivative moved to Deriv.thy. Moved ``` wenzelm@53983 ` 365` ``` theorems from Library/FDERIV.thy to Deriv.thy and base the ``` wenzelm@53983 ` 366` ``` definition of DERIV on FDERIV. Add variants of DERIV and FDERIV ``` wenzelm@53983 ` 367` ``` which are restricted to sets, i.e. to represent derivatives from ``` wenzelm@53983 ` 368` ``` left or right. ``` hoelzl@51732 ` 369` hoelzl@51732 ` 370` ``` - Removed the within-filter. It is replaced by the principal filter: ``` hoelzl@51732 ` 371` hoelzl@51732 ` 372` ``` F within X = inf F (principal X) ``` hoelzl@51732 ` 373` hoelzl@51732 ` 374` ``` - Introduce "at x within U" as a single constant, "at x" is now an ``` hoelzl@51732 ` 375` ``` abbreviation for "at x within UNIV" ``` hoelzl@51732 ` 376` wenzelm@53983 ` 377` ``` - Introduce named theorem collections tendsto_intros, ``` wenzelm@53983 ` 378` ``` continuous_intros, continuous_on_intros and FDERIV_intros. Theorems ``` wenzelm@53983 ` 379` ``` in tendsto_intros (or FDERIV_intros) are also available as ``` wenzelm@53983 ` 380` ``` tendsto_eq_intros (or FDERIV_eq_intros) where the right-hand side ``` wenzelm@53983 ` 381` ``` is replaced by a congruence rule. This allows to apply them as ``` wenzelm@53983 ` 382` ``` intro rules and then proving equivalence by the simplifier. ``` hoelzl@51732 ` 383` hoelzl@51732 ` 384` ``` - Restructured theories in HOL-Complex_Main: ``` hoelzl@51732 ` 385` hoelzl@51732 ` 386` ``` + Moved RealDef and RComplete into Real ``` hoelzl@51732 ` 387` hoelzl@51732 ` 388` ``` + Introduced Topological_Spaces and moved theorems about ``` hoelzl@51732 ` 389` ``` topological spaces, filters, limits and continuity to it ``` hoelzl@51732 ` 390` hoelzl@51732 ` 391` ``` + Renamed RealVector to Real_Vector_Spaces ``` hoelzl@51732 ` 392` wenzelm@53983 ` 393` ``` + Split Lim, SEQ, Series into Topological_Spaces, ``` wenzelm@53983 ` 394` ``` Real_Vector_Spaces, and Limits ``` hoelzl@51732 ` 395` hoelzl@51732 ` 396` ``` + Moved Ln and Log to Transcendental ``` hoelzl@51732 ` 397` hoelzl@51732 ` 398` ``` + Moved theorems about continuity from Deriv to Topological_Spaces ``` hoelzl@51732 ` 399` hoelzl@51732 ` 400` ``` - Remove various auxiliary lemmas. ``` hoelzl@51732 ` 401` hoelzl@51732 ` 402` ```INCOMPATIBILITY. ``` hoelzl@51002 ` 403` blanchet@53738 ` 404` ```* Nitpick: ``` blanchet@53803 ` 405` ``` - Added option "spy" ``` blanchet@53738 ` 406` ``` - Reduce incidence of "too high arity" errors ``` blanchet@53738 ` 407` blanchet@51137 ` 408` ```* Sledgehammer: ``` blanchet@51137 ` 409` ``` - Renamed option: ``` blanchet@51137 ` 410` ``` isar_shrink ~> isar_compress ``` blanchet@53738 ` 411` ``` INCOMPATIBILITY. ``` blanchet@53801 ` 412` ``` - Added options "isar_try0", "spy" ``` blanchet@53728 ` 413` ``` - Better support for "isar_proofs" ``` blanchet@53766 ` 414` ``` - MaSh has been fined-tuned and now runs as a local server ``` blanchet@51137 ` 415` wenzelm@54032 ` 416` ```* Improved support for ad hoc overloading of constants (see also ``` wenzelm@54032 ` 417` ```isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy). ``` wenzelm@54032 ` 418` wenzelm@54032 ` 419` ```* Library/Polynomial.thy: ``` wenzelm@54032 ` 420` ``` - Use lifting for primitive definitions. ``` wenzelm@54032 ` 421` ``` - Explicit conversions from and to lists of coefficients, used for ``` wenzelm@54032 ` 422` ``` generated code. ``` wenzelm@54032 ` 423` ``` - Replaced recursion operator poly_rec by fold_coeffs. ``` wenzelm@54032 ` 424` ``` - Prefer pre-existing gcd operation for gcd. ``` wenzelm@54032 ` 425` ``` - Fact renames: ``` wenzelm@54032 ` 426` ``` poly_eq_iff ~> poly_eq_poly_eq_iff ``` wenzelm@54032 ` 427` ``` poly_ext ~> poly_eqI ``` wenzelm@54032 ` 428` ``` expand_poly_eq ~> poly_eq_iff ``` wenzelm@54032 ` 429` ```IMCOMPATIBILITY. ``` wenzelm@54032 ` 430` wenzelm@54032 ` 431` ```* New Library/Simps_Case_Conv.thy: Provides commands simps_of_case and ``` wenzelm@54032 ` 432` ```case_of_simps to convert function definitions between a list of ``` wenzelm@54032 ` 433` ```equations with patterns on the lhs and a single equation with case ``` wenzelm@54032 ` 434` ```expressions on the rhs. See also Ex/Simps_Case_Conv_Examples.thy. ``` wenzelm@54032 ` 435` wenzelm@54032 ` 436` ```* New Library/FSet.thy: type of finite sets defined as a subtype of ``` wenzelm@54032 ` 437` ```sets defined by Lifting/Transfer. ``` wenzelm@54032 ` 438` wenzelm@54032 ` 439` ```* Discontinued theory src/HOL/Library/Eval_Witness. INCOMPATIBILITY. ``` wenzelm@54032 ` 440` wenzelm@54032 ` 441` ```* Consolidation of library theories on product orders: ``` wenzelm@54032 ` 442` wenzelm@54032 ` 443` ``` Product_Lattice ~> Product_Order -- pointwise order on products ``` wenzelm@54032 ` 444` ``` Product_ord ~> Product_Lexorder -- lexicographic order on products ``` wenzelm@54032 ` 445` wenzelm@54032 ` 446` ```INCOMPATIBILITY. ``` wenzelm@54032 ` 447` wenzelm@53160 ` 448` ```* Imperative-HOL: The MREC combinator is considered legacy and no ``` wenzelm@53160 ` 449` ```longer included by default. INCOMPATIBILITY, use partial_function ``` wenzelm@53160 ` 450` ```instead, or import theory Legacy_Mrec as a fallback. ``` wenzelm@53160 ` 451` wenzelm@53983 ` 452` ```* HOL-Algebra: Discontinued theories ~~/src/HOL/Algebra/abstract and ``` wenzelm@53983 ` 453` ```~~/src/HOL/Algebra/poly. Existing theories should be based on ``` wenzelm@53983 ` 454` ```~~/src/HOL/Library/Polynomial instead. The latter provides ``` wenzelm@53983 ` 455` ```integration with HOL's type classes for rings. INCOMPATIBILITY. ``` ballarin@51517 ` 456` wenzelm@54033 ` 457` ```* HOL-BNF: ``` wenzelm@54032 ` 458` ``` - Various improvements to BNF-based (co)datatype package, including ``` wenzelm@54032 ` 459` ``` new commands "primrec_new", "primcorec", and ``` wenzelm@54032 ` 460` ``` "datatype_new_compat", as well as documentation. See ``` wenzelm@54032 ` 461` ``` "datatypes.pdf" for details. ``` wenzelm@54032 ` 462` ``` - New "coinduction" method to avoid some boilerplate (compared to ``` wenzelm@54032 ` 463` ``` coinduct). ``` wenzelm@54032 ` 464` ``` - Renamed keywords: ``` wenzelm@54032 ` 465` ``` data ~> datatype_new ``` wenzelm@54032 ` 466` ``` codata ~> codatatype ``` wenzelm@54032 ` 467` ``` bnf_def ~> bnf ``` wenzelm@54032 ` 468` ``` - Renamed many generated theorems, including ``` wenzelm@54032 ` 469` ``` discs ~> disc ``` wenzelm@54032 ` 470` ``` map_comp' ~> map_comp ``` wenzelm@54032 ` 471` ``` map_id' ~> map_id ``` wenzelm@54032 ` 472` ``` sels ~> sel ``` wenzelm@54032 ` 473` ``` set_map' ~> set_map ``` wenzelm@54032 ` 474` ``` sets ~> set ``` wenzelm@54032 ` 475` ```IMCOMPATIBILITY. ``` wenzelm@54032 ` 476` ballarin@51517 ` 477` wenzelm@51551 ` 478` ```*** ML *** ``` wenzelm@51551 ` 479` wenzelm@53971 ` 480` ```* Spec_Check is a Quickcheck tool for Isabelle/ML. The ML function ``` wenzelm@53971 ` 481` ```"check_property" allows to check specifications of the form "ALL x y ``` wenzelm@53971 ` 482` ```z. prop x y z". See also ~~/src/Tools/Spec_Check/ with its ``` wenzelm@53971 ` 483` ```Examples.thy in particular. ``` wenzelm@53971 ` 484` wenzelm@53709 ` 485` ```* Improved printing of exception trace in Poly/ML 5.5.1, with regular ``` wenzelm@53709 ` 486` ```tracing output in the command transaction context instead of physical ``` wenzelm@53709 ` 487` ```stdout. See also Toplevel.debug, Toplevel.debugging and ``` wenzelm@53709 ` 488` ```ML_Compiler.exn_trace. ``` wenzelm@53709 ` 489` wenzelm@53971 ` 490` ```* ML type "theory" is now immutable, without any special treatment of ``` wenzelm@53971 ` 491` ```drafts or linear updates (which could lead to "stale theory" errors in ``` wenzelm@53971 ` 492` ```the past). Discontinued obsolete operations like Theory.copy, ``` wenzelm@53971 ` 493` ```Theory.checkpoint, and the auxiliary type theory_ref. Minor ``` wenzelm@53971 ` 494` ```INCOMPATIBILITY. ``` wenzelm@53164 ` 495` wenzelm@51551 ` 496` ```* More uniform naming of goal functions for skipped proofs: ``` wenzelm@51551 ` 497` wenzelm@51551 ` 498` ``` Skip_Proof.prove ~> Goal.prove_sorry ``` wenzelm@51551 ` 499` ``` Skip_Proof.prove_global ~> Goal.prove_sorry_global ``` wenzelm@51551 ` 500` wenzelm@53971 ` 501` ```Minor INCOMPATIBILITY. ``` wenzelm@51703 ` 502` wenzelm@51717 ` 503` ```* Simplifier tactics and tools use proper Proof.context instead of ``` wenzelm@51717 ` 504` ```historic type simpset. Old-style declarations like addsimps, ``` wenzelm@51717 ` 505` ```addsimprocs etc. operate directly on Proof.context. Raw type simpset ``` wenzelm@51717 ` 506` ```retains its use as snapshot of the main Simplifier context, using ``` wenzelm@51717 ` 507` ```simpset_of and put_simpset on Proof.context. INCOMPATIBILITY -- port ``` wenzelm@51717 ` 508` ```old tools by making them depend on (ctxt : Proof.context) instead of ``` wenzelm@51717 ` 509` ```(ss : simpset), then turn (simpset_of ctxt) into ctxt. ``` wenzelm@51717 ` 510` wenzelm@53971 ` 511` ```* Modifiers for classical wrappers (e.g. addWrapper, delWrapper) ``` wenzelm@53971 ` 512` ```operate on Proof.context instead of claset, for uniformity with addIs, ``` wenzelm@53971 ` 513` ```addEs, addDs etc. Note that claset_of and put_claset allow to manage ``` wenzelm@53971 ` 514` ```clasets separately from the context. ``` wenzelm@53971 ` 515` wenzelm@51717 ` 516` ```* Discontinued obsolete ML antiquotations @{claset} and @{simpset}. ``` wenzelm@51717 ` 517` ```INCOMPATIBILITY, use @{context} instead. ``` wenzelm@51717 ` 518` wenzelm@53971 ` 519` ```* Antiquotation @{theory_context A} is similar to @{theory A}, but ``` wenzelm@53971 ` 520` ```presents the result as initial Proof.context. ``` wenzelm@53971 ` 521` wenzelm@51551 ` 522` wenzelm@51398 ` 523` ```*** System *** ``` wenzelm@51398 ` 524` wenzelm@52052 ` 525` ```* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by ``` wenzelm@52052 ` 526` ```"isabelle build" in Isabelle2013. INCOMPATIBILITY. ``` wenzelm@51398 ` 527` wenzelm@52054 ` 528` ```* Discontinued obsolete isabelle-process options -f and -u (former ``` wenzelm@52054 ` 529` ```administrative aliases of option -e). Minor INCOMPATIBILITY. ``` wenzelm@52054 ` 530` wenzelm@52550 ` 531` ```* Discontinued obsolete isabelle print tool, and PRINT_COMMAND ``` wenzelm@52550 ` 532` ```settings variable. ``` wenzelm@52550 ` 533` wenzelm@52746 ` 534` ```* Discontinued ISABELLE_DOC_FORMAT settings variable and historic ``` wenzelm@52746 ` 535` ```document formats: dvi.gz, ps, ps.gz -- the default document format is ``` wenzelm@52746 ` 536` ```always pdf. ``` wenzelm@52743 ` 537` wenzelm@52053 ` 538` ```* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to ``` wenzelm@52053 ` 539` ```specify global resources of the JVM process run by isabelle build. ``` wenzelm@52053 ` 540` wenzelm@52116 ` 541` ```* Toplevel executable \$ISABELLE_HOME/bin/isabelle_scala_script allows ``` wenzelm@52116 ` 542` ```to run Isabelle/Scala source files as standalone programs. ``` wenzelm@52116 ` 543` wenzelm@52439 ` 544` ```* Improved "isabelle keywords" tool (for old-style ProofGeneral ``` wenzelm@52439 ` 545` ```keyword tables): use Isabelle/Scala operations, which inspect outer ``` wenzelm@52439 ` 546` ```syntax without requiring to build sessions first. ``` wenzelm@52439 ` 547` wenzelm@53971 ` 548` ```* Sessions may be organized via 'chapter' specifications in the ROOT ``` wenzelm@53971 ` 549` ```file, which determines a two-level hierarchy of browser info. The old ``` wenzelm@53971 ` 550` ```tree-like organization via implicit sub-session relation (with its ``` wenzelm@53971 ` 551` ```tendency towards erratic fluctuation of URLs) has been discontinued. ``` wenzelm@53971 ` 552` ```The default chapter is called "Unsorted". Potential INCOMPATIBILITY ``` wenzelm@53971 ` 553` ```for HTML presentation of theories. ``` wenzelm@53971 ` 554` wenzelm@51398 ` 555` wenzelm@51398 ` 556` wenzelm@50993 ` 557` ```New in Isabelle2013 (February 2013) ``` wenzelm@50993 ` 558` ```----------------------------------- ``` wenzelm@47887 ` 559` wenzelm@47967 ` 560` ```*** General *** ``` wenzelm@47967 ` 561` wenzelm@50126 ` 562` ```* Theorem status about oracles and unfinished/failed future proofs is ``` wenzelm@50126 ` 563` ```no longer printed by default, since it is incompatible with ``` wenzelm@50126 ` 564` ```incremental / parallel checking of the persistent document model. ML ``` wenzelm@50126 ` 565` ```function Thm.peek_status may be used to inspect a snapshot of the ``` wenzelm@50126 ` 566` ```ongoing evaluation process. Note that in batch mode --- notably ``` wenzelm@50126 ` 567` ```isabelle build --- the system ensures that future proofs of all ``` wenzelm@50126 ` 568` ```accessible theorems in the theory context are finished (as before). ``` wenzelm@50126 ` 569` wenzelm@49699 ` 570` ```* Configuration option show_markup controls direct inlining of markup ``` wenzelm@49699 ` 571` ```into the printed representation of formal entities --- notably type ``` wenzelm@49699 ` 572` ```and sort constraints. This enables Prover IDE users to retrieve that ``` wenzelm@49699 ` 573` ```information via tooltips in the output window, for example. ``` wenzelm@49699 ` 574` wenzelm@48890 ` 575` ```* Command 'ML_file' evaluates ML text from a file directly within the ``` wenzelm@48890 ` 576` ```theory, without any predeclaration via 'uses' in the theory header. ``` wenzelm@48890 ` 577` wenzelm@49243 ` 578` ```* Old command 'use' command and corresponding keyword 'uses' in the ``` wenzelm@49243 ` 579` ```theory header are legacy features and will be discontinued soon. ``` wenzelm@49243 ` 580` ```Tools that load their additional source files may imitate the ``` wenzelm@49243 ` 581` ```'ML_file' implementation, such that the system can take care of ``` wenzelm@49243 ` 582` ```dependencies properly. ``` wenzelm@49243 ` 583` wenzelm@47967 ` 584` ```* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which ``` wenzelm@47967 ` 585` ```is called fastforce / fast_force_tac already since Isabelle2011-1. ``` wenzelm@47967 ` 586` wenzelm@50110 ` 587` ```* Updated and extended "isar-ref" and "implementation" manual, reduced ``` wenzelm@50110 ` 588` ```remaining material in old "ref" manual. ``` wenzelm@48120 ` 589` wenzelm@51050 ` 590` ```* Improved support for auxiliary contexts that indicate block structure ``` wenzelm@51050 ` 591` ```for specifications. Nesting of "context fixes ... context assumes ..." ``` wenzelm@49841 ` 592` ```and "class ... context ...". ``` wenzelm@49841 ` 593` wenzelm@50772 ` 594` ```* Attribute "consumes" allows a negative value as well, which is ``` wenzelm@50778 ` 595` ```interpreted relatively to the total number of premises of the rule in ``` wenzelm@50772 ` 596` ```the target context. This form of declaration is stable when exported ``` wenzelm@50772 ` 597` ```from a nested 'context' with additional assumptions. It is the ``` wenzelm@50772 ` 598` ```preferred form for definitional packages, notably cases/rules produced ``` wenzelm@50772 ` 599` ```in HOL/inductive and HOL/function. ``` wenzelm@50772 ` 600` wenzelm@49869 ` 601` ```* More informative error messages for Isar proof commands involving ``` wenzelm@49869 ` 602` ```lazy enumerations (method applications etc.). ``` wenzelm@49869 ` 603` wenzelm@50213 ` 604` ```* Refined 'help' command to retrieve outer syntax commands according ``` wenzelm@50213 ` 605` ```to name patterns (with clickable results). ``` wenzelm@50213 ` 606` wenzelm@47967 ` 607` wenzelm@49968 ` 608` ```*** Prover IDE -- Isabelle/Scala/jEdit *** ``` wenzelm@49968 ` 609` wenzelm@49968 ` 610` ```* Parallel terminal proofs ('by') are enabled by default, likewise ``` wenzelm@49968 ` 611` ```proofs that are built into packages like 'datatype', 'function'. This ``` wenzelm@49968 ` 612` ```allows to "run ahead" checking the theory specifications on the ``` wenzelm@49968 ` 613` ```surface, while the prover is still crunching on internal ``` wenzelm@49968 ` 614` ```justifications. Unfinished / cancelled proofs are restarted as ``` wenzelm@49968 ` 615` ```required to complete full proof checking eventually. ``` wenzelm@49968 ` 616` wenzelm@49968 ` 617` ```* Improved output panel with tooltips, hyperlinks etc. based on the ``` wenzelm@49968 ` 618` ```same Rich_Text_Area as regular Isabelle/jEdit buffers. Activation of ``` wenzelm@49968 ` 619` ```tooltips leads to some window that supports the same recursively, ``` wenzelm@49968 ` 620` ```which can lead to stacks of tooltips as the semantic document content ``` wenzelm@49968 ` 621` ```is explored. ESCAPE closes the whole stack, individual windows may be ``` wenzelm@49968 ` 622` ```closed separately, or detached to become independent jEdit dockables. ``` wenzelm@49968 ` 623` wenzelm@50717 ` 624` ```* Improved support for commands that produce graph output: the text ``` wenzelm@50717 ` 625` ```message contains a clickable area to open a new instance of the graph ``` wenzelm@50717 ` 626` ```browser on demand. ``` wenzelm@50717 ` 627` wenzelm@49968 ` 628` ```* More robust incremental parsing of outer syntax (partial comments, ``` wenzelm@49968 ` 629` ```malformed symbols). Changing the balance of open/close quotes and ``` wenzelm@49968 ` 630` ```comment delimiters works more conveniently with unfinished situations ``` wenzelm@49968 ` 631` ```that frequently occur in user interaction. ``` wenzelm@49968 ` 632` wenzelm@49968 ` 633` ```* More efficient painting and improved reactivity when editing large ``` wenzelm@49968 ` 634` ```files. More scalable management of formal document content. ``` wenzelm@49968 ` 635` wenzelm@50505 ` 636` ```* Smarter handling of tracing messages: prover process pauses after ``` wenzelm@50505 ` 637` ```certain number of messages per command transaction, with some user ``` wenzelm@50505 ` 638` ```dialog to stop or continue. This avoids swamping the front-end with ``` wenzelm@50119 ` 639` ```potentially infinite message streams. ``` wenzelm@49968 ` 640` wenzelm@49968 ` 641` ```* More plugin options and preferences, based on Isabelle/Scala. The ``` wenzelm@49968 ` 642` ```jEdit plugin option panel provides access to some Isabelle/Scala ``` wenzelm@49968 ` 643` ```options, including tuning parameters for editor reactivity and color ``` wenzelm@49968 ` 644` ```schemes. ``` wenzelm@49968 ` 645` wenzelm@50184 ` 646` ```* Dockable window "Symbols" provides some editing support for Isabelle ``` wenzelm@50184 ` 647` ```symbols. ``` wenzelm@50184 ` 648` wenzelm@51082 ` 649` ```* Dockable window "Monitor" shows ML runtime statistics. Note that ``` wenzelm@51082 ` 650` ```continuous display of the chart slows down the system. ``` wenzelm@50701 ` 651` wenzelm@50183 ` 652` ```* Improved editing support for control styles: subscript, superscript, ``` wenzelm@50183 ` 653` ```bold, reset of style -- operating on single symbols or text ``` wenzelm@50198 ` 654` ```selections. Cf. keyboard shortcuts C+e DOWN/UP/RIGHT/LEFT. ``` wenzelm@50198 ` 655` wenzelm@50198 ` 656` ```* Actions isabelle.increase-font-size and isabelle.decrease-font-size ``` wenzelm@50198 ` 657` ```adjust the main text area font size, and its derivatives for output, ``` wenzelm@50836 ` 658` ```tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS, which often ``` wenzelm@50836 ` 659` ```need to be adapted to local keyboard layouts. ``` wenzelm@50183 ` 660` wenzelm@50730 ` 661` ```* More reactive completion popup by default: use \t (TAB) instead of ``` wenzelm@50730 ` 662` ```\n (NEWLINE) to minimize intrusion into regular flow of editing. See ``` wenzelm@50730 ` 663` ```also "Plugin Options / SideKick / General / Code Completion Options". ``` wenzelm@50730 ` 664` wenzelm@50406 ` 665` ```* Implicit check and build dialog of the specified logic session ``` wenzelm@50406 ` 666` ```image. For example, HOL, HOLCF, HOL-Nominal can be produced on ``` wenzelm@50406 ` 667` ```demand, without bundling big platform-dependent heap images in the ``` wenzelm@50406 ` 668` ```Isabelle distribution. ``` wenzelm@50406 ` 669` wenzelm@49968 ` 670` ```* Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates ``` wenzelm@49968 ` 671` ```from Oracle provide better multi-platform experience. This version is ``` wenzelm@49968 ` 672` ```now bundled exclusively with Isabelle. ``` wenzelm@49968 ` 673` wenzelm@49968 ` 674` wenzelm@48205 ` 675` ```*** Pure *** ``` wenzelm@48205 ` 676` haftmann@48431 ` 677` ```* Code generation for Haskell: restrict unqualified imports from ``` haftmann@48431 ` 678` ```Haskell Prelude to a small set of fundamental operations. ``` haftmann@48431 ` 679` wenzelm@50646 ` 680` ```* Command 'export_code': relative file names are interpreted ``` wenzelm@50646 ` 681` ```relatively to master directory of current theory rather than the ``` wenzelm@50646 ` 682` ```rather arbitrary current working directory. INCOMPATIBILITY. ``` haftmann@48371 ` 683` wenzelm@48205 ` 684` ```* Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, ``` wenzelm@48205 ` 685` ```use regular rule composition via "OF" / "THEN", or explicit proof ``` wenzelm@48205 ` 686` ```structure instead. Note that Isabelle/ML provides a variety of ``` wenzelm@48205 ` 687` ```operators like COMP, INCR_COMP, COMP_INCR, which need to be applied ``` wenzelm@48205 ` 688` ```with some care where this is really required. ``` wenzelm@48205 ` 689` wenzelm@48792 ` 690` ```* Command 'typ' supports an additional variant with explicit sort ``` wenzelm@48792 ` 691` ```constraint, to infer and check the most general type conforming to a ``` wenzelm@51063 ` 692` ```given sort. Example (in HOL): ``` wenzelm@48792 ` 693` wenzelm@48792 ` 694` ``` typ "_ * _ * bool * unit" :: finite ``` wenzelm@48792 ` 695` wenzelm@50716 ` 696` ```* Command 'locale_deps' visualizes all locales and their relations as ``` wenzelm@50716 ` 697` ```a Hasse diagram. ``` wenzelm@50716 ` 698` wenzelm@48205 ` 699` bulwahn@48013 ` 700` ```*** HOL *** ``` bulwahn@48013 ` 701` wenzelm@50646 ` 702` ```* Sledgehammer: ``` wenzelm@50646 ` 703` wenzelm@50646 ` 704` ``` - Added MaSh relevance filter based on machine-learning; see the ``` wenzelm@50646 ` 705` ``` Sledgehammer manual for details. ``` wenzelm@50646 ` 706` ``` - Polished Isar proofs generated with "isar_proofs" option. ``` wenzelm@50646 ` 707` ``` - Rationalized type encodings ("type_enc" option). ``` blanchet@50720 ` 708` ``` - Renamed "kill_provers" subcommand to "kill_all". ``` wenzelm@50646 ` 709` ``` - Renamed options: ``` wenzelm@50646 ` 710` ``` isar_proof ~> isar_proofs ``` wenzelm@50646 ` 711` ``` isar_shrink_factor ~> isar_shrink ``` wenzelm@50646 ` 712` ``` max_relevant ~> max_facts ``` wenzelm@50646 ` 713` ``` relevance_thresholds ~> fact_thresholds ``` wenzelm@50646 ` 714` wenzelm@50646 ` 715` ```* Quickcheck: added an optimisation for equality premises. It is ``` wenzelm@50646 ` 716` ```switched on by default, and can be switched off by setting the ``` wenzelm@50646 ` 717` ```configuration quickcheck_optimise_equality to false. ``` wenzelm@50646 ` 718` kuncar@50878 ` 719` ```* Quotient: only one quotient can be defined by quotient_type ``` kuncar@50878 ` 720` ```INCOMPATIBILITY. ``` kuncar@50878 ` 721` kuncar@50878 ` 722` ```* Lifting: ``` kuncar@50878 ` 723` ``` - generation of an abstraction function equation in lift_definition ``` kuncar@50878 ` 724` ``` - quot_del attribute ``` kuncar@50878 ` 725` ``` - renamed no_abs_code -> no_code (INCOMPATIBILITY.) ``` kuncar@50878 ` 726` wenzelm@50646 ` 727` ```* Simproc "finite_Collect" rewrites set comprehensions into pointfree ``` wenzelm@50646 ` 728` ```expressions. ``` wenzelm@50646 ` 729` wenzelm@50646 ` 730` ```* Preprocessing of the code generator rewrites set comprehensions into ``` wenzelm@50646 ` 731` ```pointfree expressions. ``` wenzelm@50646 ` 732` wenzelm@50646 ` 733` ```* The SMT solver Z3 has now by default a restricted set of directly ``` wenzelm@50646 ` 734` ```supported features. For the full set of features (div/mod, nonlinear ``` wenzelm@50646 ` 735` ```arithmetic, datatypes/records) with potential proof reconstruction ``` wenzelm@50646 ` 736` ```failures, enable the configuration option "z3_with_extensions". Minor ``` wenzelm@50646 ` 737` ```INCOMPATIBILITY. ``` haftmann@49948 ` 738` wenzelm@49836 ` 739` ```* Simplified 'typedef' specifications: historical options for implicit ``` wenzelm@49836 ` 740` ```set definition and alternative name have been discontinued. The ``` wenzelm@49836 ` 741` ```former behavior of "typedef (open) t = A" is now the default, but ``` wenzelm@49836 ` 742` ```written just "typedef t = A". INCOMPATIBILITY, need to adapt theories ``` wenzelm@49836 ` 743` ```accordingly. ``` wenzelm@49836 ` 744` wenzelm@50646 ` 745` ```* Removed constant "chars"; prefer "Enum.enum" on type "char" ``` wenzelm@50646 ` 746` ```directly. INCOMPATIBILITY. ``` wenzelm@50646 ` 747` wenzelm@50646 ` 748` ```* Moved operation product, sublists and n_lists from theory Enum to ``` wenzelm@50646 ` 749` ```List. INCOMPATIBILITY. ``` haftmann@49822 ` 750` haftmann@49739 ` 751` ```* Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. ``` haftmann@49739 ` 752` haftmann@49738 ` 753` ```* Class "comm_monoid_diff" formalises properties of bounded ``` haftmann@49388 ` 754` ```subtraction, with natural numbers and multisets as typical instances. ``` haftmann@49388 ` 755` wenzelm@50646 ` 756` ```* Added combinator "Option.these" with type "'a option set => 'a set". ``` wenzelm@50646 ` 757` wenzelm@50646 ` 758` ```* Theory "Transitive_Closure": renamed lemmas ``` wenzelm@50646 ` 759` wenzelm@50646 ` 760` ``` reflcl_tranclp -> reflclp_tranclp ``` wenzelm@50646 ` 761` ``` rtranclp_reflcl -> rtranclp_reflclp ``` wenzelm@50646 ` 762` wenzelm@50646 ` 763` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 764` wenzelm@50646 ` 765` ```* Theory "Rings": renamed lemmas (in class semiring) ``` wenzelm@50646 ` 766` wenzelm@50646 ` 767` ``` left_distrib ~> distrib_right ``` wenzelm@50646 ` 768` ``` right_distrib ~> distrib_left ``` wenzelm@50646 ` 769` wenzelm@50646 ` 770` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 771` wenzelm@50646 ` 772` ```* Generalized the definition of limits: ``` wenzelm@50646 ` 773` wenzelm@50646 ` 774` ``` - Introduced the predicate filterlim (LIM x F. f x :> G) which ``` wenzelm@50646 ` 775` ``` expresses that when the input values x converge to F then the ``` wenzelm@50646 ` 776` ``` output f x converges to G. ``` wenzelm@50646 ` 777` wenzelm@50646 ` 778` ``` - Added filters for convergence to positive (at_top) and negative ``` wenzelm@50646 ` 779` ``` infinity (at_bot). ``` wenzelm@50646 ` 780` wenzelm@50646 ` 781` ``` - Moved infinity in the norm (at_infinity) from ``` wenzelm@50646 ` 782` ``` Multivariate_Analysis to Complex_Main. ``` wenzelm@50646 ` 783` wenzelm@50646 ` 784` ``` - Removed real_tendsto_inf, it is superseded by "LIM x F. f x :> ``` wenzelm@50646 ` 785` ``` at_top". ``` wenzelm@50646 ` 786` wenzelm@50646 ` 787` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 788` wenzelm@50646 ` 789` ```* Theory "Library/Option_ord" provides instantiation of option type to ``` wenzelm@50646 ` 790` ```lattice type classes. ``` wenzelm@50646 ` 791` wenzelm@50646 ` 792` ```* Theory "Library/Multiset": renamed ``` wenzelm@50646 ` 793` wenzelm@50646 ` 794` ``` constant fold_mset ~> Multiset.fold ``` wenzelm@50646 ` 795` ``` fact fold_mset_commute ~> fold_mset_comm ``` wenzelm@50646 ` 796` wenzelm@50646 ` 797` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 798` wenzelm@50646 ` 799` ```* Renamed theory Library/List_Prefix to Library/Sublist, with related ``` wenzelm@50646 ` 800` ```changes as follows. ``` wenzelm@50646 ` 801` wenzelm@50646 ` 802` ``` - Renamed constants (and related lemmas) ``` Christian@49145 ` 803` Christian@49145 ` 804` ``` prefix ~> prefixeq ``` Christian@49145 ` 805` ``` strict_prefix ~> prefix ``` Christian@49145 ` 806` wenzelm@50646 ` 807` ``` - Replaced constant "postfix" by "suffixeq" with swapped argument ``` wenzelm@50646 ` 808` ``` order (i.e., "postfix xs ys" is now "suffixeq ys xs") and dropped ``` wenzelm@50646 ` 809` ``` old infix syntax "xs >>= ys"; use "suffixeq ys xs" instead. ``` wenzelm@50646 ` 810` ``` Renamed lemmas accordingly. ``` wenzelm@50646 ` 811` wenzelm@50646 ` 812` ``` - Added constant "list_hembeq" for homeomorphic embedding on ``` wenzelm@50646 ` 813` ``` lists. Added abbreviation "sublisteq" for special case ``` wenzelm@50646 ` 814` ``` "list_hembeq (op =)". ``` wenzelm@50646 ` 815` wenzelm@50646 ` 816` ``` - Theory Library/Sublist no longer provides "order" and "bot" type ``` wenzelm@50646 ` 817` ``` class instances for the prefix order (merely corresponding locale ``` wenzelm@50646 ` 818` ``` interpretations). The type class instances are now in theory ``` wenzelm@50646 ` 819` ``` Library/Prefix_Order. ``` wenzelm@50646 ` 820` wenzelm@50646 ` 821` ``` - The sublist relation of theory Library/Sublist_Order is now based ``` wenzelm@50646 ` 822` ``` on "Sublist.sublisteq". Renamed lemmas accordingly: ``` Christian@50516 ` 823` Christian@50516 ` 824` ``` le_list_append_le_same_iff ~> Sublist.sublisteq_append_le_same_iff ``` Christian@50516 ` 825` ``` le_list_append_mono ~> Sublist.list_hembeq_append_mono ``` Christian@50516 ` 826` ``` le_list_below_empty ~> Sublist.list_hembeq_Nil, Sublist.list_hembeq_Nil2 ``` Christian@50516 ` 827` ``` le_list_Cons_EX ~> Sublist.list_hembeq_ConsD ``` Christian@50516 ` 828` ``` le_list_drop_Cons2 ~> Sublist.sublisteq_Cons2' ``` Christian@50516 ` 829` ``` le_list_drop_Cons_neq ~> Sublist.sublisteq_Cons2_neq ``` Christian@50516 ` 830` ``` le_list_drop_Cons ~> Sublist.sublisteq_Cons' ``` Christian@50516 ` 831` ``` le_list_drop_many ~> Sublist.sublisteq_drop_many ``` Christian@50516 ` 832` ``` le_list_filter_left ~> Sublist.sublisteq_filter_left ``` Christian@50516 ` 833` ``` le_list_rev_drop_many ~> Sublist.sublisteq_rev_drop_many ``` Christian@50516 ` 834` ``` le_list_rev_take_iff ~> Sublist.sublisteq_append ``` Christian@50516 ` 835` ``` le_list_same_length ~> Sublist.sublisteq_same_length ``` Christian@50516 ` 836` ``` le_list_take_many_iff ~> Sublist.sublisteq_append' ``` Christian@49145 ` 837` ``` less_eq_list.drop ~> less_eq_list_drop ``` Christian@49145 ` 838` ``` less_eq_list.induct ~> less_eq_list_induct ``` Christian@50516 ` 839` ``` not_le_list_length ~> Sublist.not_sublisteq_length ``` Christian@49145 ` 840` wenzelm@50646 ` 841` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 842` wenzelm@50646 ` 843` ```* New theory Library/Countable_Set. ``` wenzelm@50646 ` 844` wenzelm@50646 ` 845` ```* Theory Library/Debug and Library/Parallel provide debugging and ``` wenzelm@50646 ` 846` ```parallel execution for code generated towards Isabelle/ML. ``` wenzelm@50646 ` 847` wenzelm@50646 ` 848` ```* Theory Library/FuncSet: Extended support for Pi and extensional and ``` wenzelm@50646 ` 849` ```introduce the extensional dependent function space "PiE". Replaced ``` wenzelm@50646 ` 850` ```extensional_funcset by an abbreviation, and renamed lemmas from ``` wenzelm@50646 ` 851` ```extensional_funcset to PiE as follows: ``` wenzelm@50646 ` 852` wenzelm@50646 ` 853` ``` extensional_empty ~> PiE_empty ``` wenzelm@50646 ` 854` ``` extensional_funcset_empty_domain ~> PiE_empty_domain ``` wenzelm@50646 ` 855` ``` extensional_funcset_empty_range ~> PiE_empty_range ``` wenzelm@50646 ` 856` ``` extensional_funcset_arb ~> PiE_arb ``` wenzelm@50646 ` 857` ``` extensional_funcset_mem ~> PiE_mem ``` wenzelm@50646 ` 858` ``` extensional_funcset_extend_domainI ~> PiE_fun_upd ``` wenzelm@50646 ` 859` ``` extensional_funcset_restrict_domain ~> fun_upd_in_PiE ``` wenzelm@50646 ` 860` ``` extensional_funcset_extend_domain_eq ~> PiE_insert_eq ``` wenzelm@50646 ` 861` ``` card_extensional_funcset ~> card_PiE ``` wenzelm@50646 ` 862` ``` finite_extensional_funcset ~> finite_PiE ``` wenzelm@50646 ` 863` wenzelm@50646 ` 864` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 865` wenzelm@50646 ` 866` ```* Theory Library/FinFun: theory of almost everywhere constant ``` wenzelm@50646 ` 867` ```functions (supersedes the AFP entry "Code Generation for Functions as ``` wenzelm@50646 ` 868` ```Data"). ``` wenzelm@50646 ` 869` wenzelm@50646 ` 870` ```* Theory Library/Phantom: generic phantom type to make a type ``` wenzelm@50646 ` 871` ```parameter appear in a constant's type. This alternative to adding ``` wenzelm@50646 ` 872` ```TYPE('a) as another parameter avoids unnecessary closures in generated ``` wenzelm@50646 ` 873` ```code. ``` wenzelm@50646 ` 874` wenzelm@50646 ` 875` ```* Theory Library/RBT_Impl: efficient construction of red-black trees ``` wenzelm@50646 ` 876` ```from sorted associative lists. Merging two trees with rbt_union may ``` wenzelm@50646 ` 877` ```return a structurally different tree than before. Potential ``` wenzelm@50646 ` 878` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 879` wenzelm@50646 ` 880` ```* Theory Library/IArray: immutable arrays with code generation. ``` wenzelm@50646 ` 881` wenzelm@50646 ` 882` ```* Theory Library/Finite_Lattice: theory of finite lattices. ``` wenzelm@50646 ` 883` wenzelm@50646 ` 884` ```* HOL/Multivariate_Analysis: replaced ``` wenzelm@50646 ` 885` wenzelm@50646 ` 886` ``` "basis :: 'a::euclidean_space => nat => real" ``` wenzelm@50646 ` 887` ``` "\\ :: (nat => real) => 'a::euclidean_space" ``` wenzelm@50646 ` 888` wenzelm@50646 ` 889` ```on euclidean spaces by using the inner product "_ \ _" with ``` wenzelm@50646 ` 890` ```vectors from the Basis set: "\\ i. f i" is superseded by ``` wenzelm@50646 ` 891` ```"SUM i : Basis. f i * r i". ``` wenzelm@50646 ` 892` wenzelm@50646 ` 893` ``` With this change the following constants are also changed or removed: ``` wenzelm@50646 ` 894` wenzelm@50646 ` 895` ``` DIM('a) :: nat ~> card (Basis :: 'a set) (is an abbreviation) ``` wenzelm@50646 ` 896` ``` a \$\$ i ~> inner a i (where i : Basis) ``` wenzelm@50646 ` 897` ``` cart_base i removed ``` wenzelm@50646 ` 898` ``` \, \' removed ``` hoelzl@50526 ` 899` hoelzl@50526 ` 900` ``` Theorems about these constants where removed. ``` hoelzl@50526 ` 901` hoelzl@50526 ` 902` ``` Renamed lemmas: ``` hoelzl@50526 ` 903` wenzelm@50646 ` 904` ``` component_le_norm ~> Basis_le_norm ``` wenzelm@50646 ` 905` ``` euclidean_eq ~> euclidean_eq_iff ``` wenzelm@50646 ` 906` ``` differential_zero_maxmin_component ~> differential_zero_maxmin_cart ``` wenzelm@50646 ` 907` ``` euclidean_simps ~> inner_simps ``` wenzelm@50646 ` 908` ``` independent_basis ~> independent_Basis ``` wenzelm@50646 ` 909` ``` span_basis ~> span_Basis ``` wenzelm@50646 ` 910` ``` in_span_basis ~> in_span_Basis ``` wenzelm@50646 ` 911` ``` norm_bound_component_le ~> norm_boound_Basis_le ``` wenzelm@50646 ` 912` ``` norm_bound_component_lt ~> norm_boound_Basis_lt ``` wenzelm@50646 ` 913` ``` component_le_infnorm ~> Basis_le_infnorm ``` wenzelm@50646 ` 914` wenzelm@50646 ` 915` ```INCOMPATIBILITY. ``` hoelzl@50526 ` 916` hoelzl@50141 ` 917` ```* HOL/Probability: ``` wenzelm@50646 ` 918` wenzelm@50646 ` 919` ``` - Added simproc "measurable" to automatically prove measurability. ``` wenzelm@50646 ` 920` wenzelm@50646 ` 921` ``` - Added induction rules for sigma sets with disjoint union ``` wenzelm@50646 ` 922` ``` (sigma_sets_induct_disjoint) and for Borel-measurable functions ``` wenzelm@50646 ` 923` ``` (borel_measurable_induct). ``` wenzelm@50646 ` 924` wenzelm@50646 ` 925` ``` - Added the Daniell-Kolmogorov theorem (the existence the limit of a ``` wenzelm@50646 ` 926` ``` projective family). ``` wenzelm@50646 ` 927` wenzelm@50646 ` 928` ```* HOL/Cardinals: Theories of ordinals and cardinals (supersedes the ``` wenzelm@50646 ` 929` ```AFP entry "Ordinals_and_Cardinals"). ``` wenzelm@50646 ` 930` wenzelm@50646 ` 931` ```* HOL/BNF: New (co)datatype package based on bounded natural functors ``` wenzelm@50646 ` 932` ```with support for mixed, nested recursion and interesting non-free ``` wenzelm@50646 ` 933` ```datatypes. ``` blanchet@48094 ` 934` wenzelm@50991 ` 935` ```* HOL/Finite_Set and Relation: added new set and relation operations ``` kuncar@50878 ` 936` ```expressed by Finite_Set.fold. ``` kuncar@50878 ` 937` kuncar@50878 ` 938` ```* New theory HOL/Library/RBT_Set: implementation of sets by red-black ``` kuncar@50878 ` 939` ```trees for the code generator. ``` kuncar@50878 ` 940` kuncar@50878 ` 941` ```* HOL/Library/RBT and HOL/Library/Mapping have been converted to ``` kuncar@50878 ` 942` ```Lifting/Transfer. ``` kuncar@50878 ` 943` ```possible INCOMPATIBILITY. ``` kuncar@50878 ` 944` kuncar@50878 ` 945` ```* HOL/Set: renamed Set.project -> Set.filter ``` kuncar@50878 ` 946` ```INCOMPATIBILITY. ``` kuncar@50878 ` 947` wenzelm@48120 ` 948` wenzelm@48206 ` 949` ```*** Document preparation *** ``` wenzelm@48206 ` 950` wenzelm@50646 ` 951` ```* Dropped legacy antiquotations "term_style" and "thm_style", since ``` wenzelm@50646 ` 952` ```styles may be given as arguments to "term" and "thm" already. ``` wenzelm@50646 ` 953` ```Discontinued legacy styles "prem1" .. "prem19". ``` wenzelm@50646 ` 954` wenzelm@50646 ` 955` ```* Default LaTeX rendering for \ is now based on eurosym package, ``` wenzelm@50646 ` 956` ```instead of slightly exotic babel/greek. ``` wenzelm@48206 ` 957` wenzelm@48616 ` 958` ```* Document variant NAME may use different LaTeX entry point ``` wenzelm@48616 ` 959` ```document/root_NAME.tex if that file exists, instead of the common ``` wenzelm@48616 ` 960` ```document/root.tex. ``` wenzelm@48616 ` 961` wenzelm@48657 ` 962` ```* Simplified custom document/build script, instead of old-style ``` wenzelm@48657 ` 963` ```document/IsaMakefile. Minor INCOMPATIBILITY. ``` wenzelm@48657 ` 964` wenzelm@48206 ` 965` wenzelm@48992 ` 966` ```*** ML *** ``` wenzelm@48992 ` 967` wenzelm@50646 ` 968` ```* The default limit for maximum number of worker threads is now 8, ``` wenzelm@50646 ` 969` ```instead of 4, in correspondence to capabilities of contemporary ``` wenzelm@50646 ` 970` ```hardware and Poly/ML runtime system. ``` wenzelm@50646 ` 971` wenzelm@49869 ` 972` ```* Type Seq.results and related operations support embedded error ``` wenzelm@49869 ` 973` ```messages within lazy enumerations, and thus allow to provide ``` wenzelm@49869 ` 974` ```informative errors in the absence of any usable results. ``` wenzelm@49869 ` 975` wenzelm@48992 ` 976` ```* Renamed Position.str_of to Position.here to emphasize that this is a ``` wenzelm@48992 ` 977` ```formal device to inline positions into message text, but not ``` wenzelm@48992 ` 978` ```necessarily printing visible text. ``` wenzelm@48992 ` 979` wenzelm@48992 ` 980` wenzelm@48206 ` 981` ```*** System *** ``` wenzelm@48206 ` 982` wenzelm@48585 ` 983` ```* Advanced support for Isabelle sessions and build management, see ``` wenzelm@48585 ` 984` ```"system" manual for the chapter of that name, especially the "isabelle ``` wenzelm@51056 ` 985` ```build" tool and its examples. The "isabelle mkroot" tool prepares ``` wenzelm@51056 ` 986` ```session root directories for use with "isabelle build", similar to ``` wenzelm@51056 ` 987` ```former "isabelle mkdir" for "isabelle usedir". Note that this affects ``` wenzelm@51056 ` 988` ```document preparation as well. INCOMPATIBILITY, isabelle usedir / ``` wenzelm@48736 ` 989` ```mkdir / make are rendered obsolete. ``` wenzelm@48736 ` 990` wenzelm@51056 ` 991` ```* Discontinued obsolete Isabelle/build script, it is superseded by the ``` wenzelm@51056 ` 992` ```regular isabelle build tool. For example: ``` wenzelm@51056 ` 993` wenzelm@51056 ` 994` ``` isabelle build -s -b HOL ``` wenzelm@51056 ` 995` wenzelm@48736 ` 996` ```* Discontinued obsolete "isabelle makeall". ``` wenzelm@48585 ` 997` wenzelm@48722 ` 998` ```* Discontinued obsolete IsaMakefile and ROOT.ML files from the ``` wenzelm@48722 ` 999` ```Isabelle distribution, except for rudimentary src/HOL/IsaMakefile that ``` wenzelm@48722 ` 1000` ```provides some traditional targets that invoke "isabelle build". Note ``` wenzelm@48722 ` 1001` ```that this is inefficient! Applications of Isabelle/HOL involving ``` wenzelm@48722 ` 1002` ```"isabelle make" should be upgraded to use "isabelle build" directly. ``` wenzelm@48722 ` 1003` wenzelm@48693 ` 1004` ```* The "isabelle options" tool prints Isabelle system options, as ``` wenzelm@48693 ` 1005` ```required for "isabelle build", for example. ``` wenzelm@48693 ` 1006` wenzelm@50646 ` 1007` ```* The "isabelle logo" tool produces EPS and PDF format simultaneously. ``` wenzelm@50646 ` 1008` ```Minor INCOMPATIBILITY in command-line options. ``` wenzelm@50646 ` 1009` wenzelm@50646 ` 1010` ```* The "isabelle install" tool has now a simpler command-line. Minor ``` wenzelm@50646 ` 1011` ```INCOMPATIBILITY. ``` wenzelm@50646 ` 1012` wenzelm@48844 ` 1013` ```* The "isabelle components" tool helps to resolve add-on components ``` wenzelm@48844 ` 1014` ```that are not bundled, or referenced from a bare-bones repository ``` wenzelm@48844 ` 1015` ```version of Isabelle. ``` wenzelm@48844 ` 1016` wenzelm@50646 ` 1017` ```* Settings variable ISABELLE_PLATFORM_FAMILY refers to the general ``` wenzelm@50646 ` 1018` ```platform family: "linux", "macos", "windows". ``` wenzelm@50646 ` 1019` wenzelm@50646 ` 1020` ```* The ML system is configured as regular component, and no longer ``` wenzelm@50646 ` 1021` ```picked up from some surrounding directory. Potential INCOMPATIBILITY ``` wenzelm@50646 ` 1022` ```for home-made settings. ``` wenzelm@50132 ` 1023` wenzelm@50701 ` 1024` ```* Improved ML runtime statistics (heap, threads, future tasks etc.). ``` wenzelm@50701 ` 1025` wenzelm@48206 ` 1026` ```* Discontinued support for Poly/ML 5.2.1, which was the last version ``` wenzelm@48206 ` 1027` ```without exception positions and advanced ML compiler/toplevel ``` wenzelm@48206 ` 1028` ```configuration. ``` wenzelm@48206 ` 1029` wenzelm@48574 ` 1030` ```* Discontinued special treatment of Proof General -- no longer guess ``` wenzelm@48574 ` 1031` ```PROOFGENERAL_HOME based on accidental file-system layout. Minor ``` wenzelm@48574 ` 1032` ```INCOMPATIBILITY: provide PROOFGENERAL_HOME and PROOFGENERAL_OPTIONS ``` wenzelm@48574 ` 1033` ```settings manually, or use a Proof General version that has been ``` wenzelm@48574 ` 1034` ```bundled as Isabelle component. ``` wenzelm@48206 ` 1035` wenzelm@50182 ` 1036` wenzelm@48120 ` 1037` wenzelm@47462 ` 1038` ```New in Isabelle2012 (May 2012) ``` wenzelm@47462 ` 1039` ```------------------------------ ``` wenzelm@45109 ` 1040` wenzelm@45593 ` 1041` ```*** General *** ``` wenzelm@45593 ` 1042` wenzelm@45614 ` 1043` ```* Prover IDE (PIDE) improvements: ``` wenzelm@45614 ` 1044` wenzelm@47585 ` 1045` ``` - more robust Sledgehammer integration (as before the sledgehammer ``` wenzelm@47806 ` 1046` ``` command-line needs to be typed into the source buffer) ``` wenzelm@45614 ` 1047` ``` - markup for bound variables ``` wenzelm@47806 ` 1048` ``` - markup for types of term variables (displayed as tooltips) ``` wenzelm@46956 ` 1049` ``` - support for user-defined Isar commands within the running session ``` wenzelm@47158 ` 1050` ``` - improved support for Unicode outside original 16bit range ``` wenzelm@47158 ` 1051` ``` e.g. glyph for \ (thanks to jEdit 4.5.1) ``` wenzelm@45614 ` 1052` wenzelm@47806 ` 1053` ```* Forward declaration of outer syntax keywords within the theory ``` wenzelm@47806 ` 1054` ```header -- minor INCOMPATIBILITY for user-defined commands. Allow new ``` wenzelm@47806 ` 1055` ```commands to be used in the same theory where defined. ``` wenzelm@46485 ` 1056` wenzelm@47482 ` 1057` ```* Auxiliary contexts indicate block structure for specifications with ``` wenzelm@47482 ` 1058` ```additional parameters and assumptions. Such unnamed contexts may be ``` wenzelm@47482 ` 1059` ```nested within other targets, like 'theory', 'locale', 'class', ``` wenzelm@47482 ` 1060` ```'instantiation' etc. Results from the local context are generalized ``` wenzelm@47482 ` 1061` ```accordingly and applied to the enclosing target context. Example: ``` wenzelm@47482 ` 1062` wenzelm@47482 ` 1063` ``` context ``` wenzelm@47482 ` 1064` ``` fixes x y z :: 'a ``` wenzelm@47482 ` 1065` ``` assumes xy: "x = y" and yz: "y = z" ``` wenzelm@47482 ` 1066` ``` begin ``` wenzelm@47482 ` 1067` wenzelm@47482 ` 1068` ``` lemma my_trans: "x = z" using xy yz by simp ``` wenzelm@47482 ` 1069` wenzelm@47482 ` 1070` ``` end ``` wenzelm@47482 ` 1071` wenzelm@47482 ` 1072` ``` thm my_trans ``` wenzelm@47482 ` 1073` wenzelm@47482 ` 1074` ```The most basic application is to factor-out context elements of ``` wenzelm@47482 ` 1075` ```several fixes/assumes/shows theorem statements, e.g. see ``` wenzelm@47482 ` 1076` ```~~/src/HOL/Isar_Examples/Group_Context.thy ``` wenzelm@47482 ` 1077` wenzelm@47482 ` 1078` ```Any other local theory specification element works within the "context ``` wenzelm@47482 ` 1079` ```... begin ... end" block as well. ``` wenzelm@47482 ` 1080` wenzelm@47484 ` 1081` ```* Bundled declarations associate attributed fact expressions with a ``` wenzelm@47484 ` 1082` ```given name in the context. These may be later included in other ``` wenzelm@47484 ` 1083` ```contexts. This allows to manage context extensions casually, without ``` wenzelm@47855 ` 1084` ```the logical dependencies of locales and locale interpretation. See ``` wenzelm@47855 ` 1085` ```commands 'bundle', 'include', 'including' etc. in the isar-ref manual. ``` wenzelm@47484 ` 1086` wenzelm@47829 ` 1087` ```* Commands 'lemmas' and 'theorems' allow local variables using 'for' ``` wenzelm@47829 ` 1088` ```declaration, and results are standardized before being stored. Thus ``` wenzelm@47829 ` 1089` ```old-style "standard" after instantiation or composition of facts ``` wenzelm@47829 ` 1090` ```becomes obsolete. Minor INCOMPATIBILITY, due to potential change of ``` wenzelm@47829 ` 1091` ```indices of schematic variables. ``` wenzelm@47829 ` 1092` wenzelm@47829 ` 1093` ```* Rule attributes in local theory declarations (e.g. locale or class) ``` wenzelm@47829 ` 1094` ```are now statically evaluated: the resulting theorem is stored instead ``` wenzelm@47829 ` 1095` ```of the original expression. INCOMPATIBILITY in rare situations, where ``` wenzelm@47829 ` 1096` ```the historic accident of dynamic re-evaluation in interpretations ``` wenzelm@47829 ` 1097` ```etc. was exploited. ``` wenzelm@47829 ` 1098` wenzelm@47829 ` 1099` ```* New tutorial "Programming and Proving in Isabelle/HOL" ``` wenzelm@47829 ` 1100` ```("prog-prove"). It completely supersedes "A Tutorial Introduction to ``` wenzelm@47829 ` 1101` ```Structured Isar Proofs" ("isar-overview"), which has been removed. It ``` wenzelm@47829 ` 1102` ```also supersedes "Isabelle/HOL, A Proof Assistant for Higher-Order ``` wenzelm@47829 ` 1103` ```Logic" as the recommended beginners tutorial, but does not cover all ``` wenzelm@47829 ` 1104` ```of the material of that old tutorial. ``` wenzelm@47829 ` 1105` wenzelm@47829 ` 1106` ```* Updated and extended reference manuals: "isar-ref", ``` wenzelm@47829 ` 1107` ```"implementation", "system"; reduced remaining material in old "ref" ``` wenzelm@47829 ` 1108` ```manual. ``` wenzelm@47829 ` 1109` wenzelm@47829 ` 1110` wenzelm@47829 ` 1111` ```*** Pure *** ``` wenzelm@47829 ` 1112` wenzelm@46976 ` 1113` ```* Command 'definition' no longer exports the foundational "raw_def" ``` wenzelm@46976 ` 1114` ```into the user context. Minor INCOMPATIBILITY, may use the regular ``` wenzelm@46976 ` 1115` ```"def" result with attribute "abs_def" to imitate the old version. ``` wenzelm@46976 ` 1116` wenzelm@47855 ` 1117` ```* Attribute "abs_def" turns an equation of the form "f x y == t" into ``` wenzelm@47855 ` 1118` ```"f == %x y. t", which ensures that "simp" or "unfold" steps always ``` wenzelm@47855 ` 1119` ```expand it. This also works for object-logic equality. (Formerly ``` wenzelm@47855 ` 1120` ```undocumented feature.) ``` wenzelm@47855 ` 1121` wenzelm@47856 ` 1122` ```* Sort constraints are now propagated in simultaneous statements, just ``` wenzelm@47856 ` 1123` ```like type constraints. INCOMPATIBILITY in rare situations, where ``` wenzelm@47856 ` 1124` ```distinct sorts used to be assigned accidentally. For example: ``` wenzelm@47856 ` 1125` wenzelm@47856 ` 1126` ``` lemma "P (x::'a::foo)" and "Q (y::'a::bar)" -- "now illegal" ``` wenzelm@47856 ` 1127` wenzelm@47856 ` 1128` ``` lemma "P (x::'a)" and "Q (y::'a::bar)" ``` wenzelm@47856 ` 1129` ``` -- "now uniform 'a::bar instead of default sort for first occurrence (!)" ``` wenzelm@47856 ` 1130` wenzelm@47856 ` 1131` ```* Rule composition via attribute "OF" (or ML functions OF/MRS) is more ``` wenzelm@47856 ` 1132` ```tolerant against multiple unifiers, as long as the final result is ``` wenzelm@47856 ` 1133` ```unique. (As before, rules are composed in canonical right-to-left ``` wenzelm@47856 ` 1134` ```order to accommodate newly introduced premises.) ``` wenzelm@47856 ` 1135` wenzelm@47806 ` 1136` ```* Renamed some inner syntax categories: ``` wenzelm@47806 ` 1137` wenzelm@47806 ` 1138` ``` num ~> num_token ``` wenzelm@47806 ` 1139` ``` xnum ~> xnum_token ``` wenzelm@47806 ` 1140` ``` xstr ~> str_token ``` wenzelm@47806 ` 1141` wenzelm@47806 ` 1142` ```Minor INCOMPATIBILITY. Note that in practice "num_const" or ``` wenzelm@47806 ` 1143` ```"num_position" etc. are mainly used instead (which also include ``` wenzelm@47806 ` 1144` ```position information via constraints). ``` wenzelm@47806 ` 1145` wenzelm@47829 ` 1146` ```* Simplified configuration options for syntax ambiguity: see ``` wenzelm@47829 ` 1147` ```"syntax_ambiguity_warning" and "syntax_ambiguity_limit" in isar-ref ``` wenzelm@47829 ` 1148` ```manual. Minor INCOMPATIBILITY. ``` wenzelm@47829 ` 1149` wenzelm@47856 ` 1150` ```* Discontinued configuration option "syntax_positions": atomic terms ``` wenzelm@47856 ` 1151` ```in parse trees are always annotated by position constraints. ``` wenzelm@45134 ` 1152` wenzelm@47464 ` 1153` ```* Old code generator for SML and its commands 'code_module', ``` wenzelm@45383 ` 1154` ```'code_library', 'consts_code', 'types_code' have been discontinued. ``` haftmann@46028 ` 1155` ```Use commands of the generic code generator instead. INCOMPATIBILITY. ``` wenzelm@45383 ` 1156` wenzelm@47464 ` 1157` ```* Redundant attribute "code_inline" has been discontinued. Use ``` wenzelm@47464 ` 1158` ```"code_unfold" instead. INCOMPATIBILITY. ``` wenzelm@47464 ` 1159` wenzelm@47464 ` 1160` ```* Dropped attribute "code_unfold_post" in favor of the its dual ``` wenzelm@47464 ` 1161` ```"code_abbrev", which yields a common pattern in definitions like ``` haftmann@46028 ` 1162` haftmann@46028 ` 1163` ``` definition [code_abbrev]: "f = t" ``` haftmann@46028 ` 1164` haftmann@46028 ` 1165` ```INCOMPATIBILITY. ``` wenzelm@45383 ` 1166` wenzelm@47856 ` 1167` ```* Obsolete 'types' command has been discontinued. Use 'type_synonym' ``` wenzelm@47856 ` 1168` ```instead. INCOMPATIBILITY. ``` wenzelm@47856 ` 1169` wenzelm@47856 ` 1170` ```* Discontinued old "prems" fact, which used to refer to the accidental ``` wenzelm@47856 ` 1171` ```collection of foundational premises in the context (already marked as ``` wenzelm@47856 ` 1172` ```legacy since Isabelle2011). ``` wenzelm@47855 ` 1173` wenzelm@45427 ` 1174` huffman@45122 ` 1175` ```*** HOL *** ``` huffman@45122 ` 1176` wenzelm@47464 ` 1177` ```* Type 'a set is now a proper type constructor (just as before ``` wenzelm@47464 ` 1178` ```Isabelle2008). Definitions mem_def and Collect_def have disappeared. ``` wenzelm@47464 ` 1179` ```Non-trivial INCOMPATIBILITY. For developments keeping predicates and ``` wenzelm@47855 ` 1180` ```sets separate, it is often sufficient to rephrase some set S that has ``` wenzelm@47855 ` 1181` ```been accidentally used as predicates by "%x. x : S", and some ``` wenzelm@47855 ` 1182` ```predicate P that has been accidentally used as set by "{x. P x}". ``` wenzelm@47855 ` 1183` ```Corresponding proofs in a first step should be pruned from any ``` wenzelm@47855 ` 1184` ```tinkering with former theorems mem_def and Collect_def as far as ``` wenzelm@47855 ` 1185` ```possible. ``` wenzelm@47855 ` 1186` wenzelm@47855 ` 1187` ```For developments which deliberately mix predicates and sets, a ``` wenzelm@47464 ` 1188` ```planning step is necessary to determine what should become a predicate ``` wenzelm@47464 ` 1189` ```and what a set. It can be helpful to carry out that step in ``` wenzelm@47464 ` 1190` ```Isabelle2011-1 before jumping right into the current release. ``` wenzelm@47464 ` 1191` wenzelm@47855 ` 1192` ```* Code generation by default implements sets as container type rather ``` wenzelm@47855 ` 1193` ```than predicates. INCOMPATIBILITY. ``` wenzelm@47855 ` 1194` wenzelm@47855 ` 1195` ```* New type synonym 'a rel = ('a * 'a) set ``` wenzelm@47855 ` 1196` wenzelm@47464 ` 1197` ```* The representation of numerals has changed. Datatype "num" ``` wenzelm@47464 ` 1198` ```represents strictly positive binary numerals, along with functions ``` wenzelm@47464 ` 1199` ```"numeral :: num => 'a" and "neg_numeral :: num => 'a" to represent ``` wenzelm@47855 ` 1200` ```positive and negated numeric literals, respectively. See also ``` wenzelm@47855 ` 1201` ```definitions in ~~/src/HOL/Num.thy. Potential INCOMPATIBILITY, some ``` wenzelm@47855 ` 1202` ```user theories may require adaptations as follows: ``` huffman@47108 ` 1203` huffman@47108 ` 1204` ``` - Theorems with number_ring or number_semiring constraints: These ``` huffman@47108 ` 1205` ``` classes are gone; use comm_ring_1 or comm_semiring_1 instead. ``` huffman@47108 ` 1206` huffman@47108 ` 1207` ``` - Theories defining numeric types: Remove number, number_semiring, ``` huffman@47108 ` 1208` ``` and number_ring instances. Defer all theorems about numerals until ``` huffman@47108 ` 1209` ``` after classes one and semigroup_add have been instantiated. ``` huffman@47108 ` 1210` huffman@47108 ` 1211` ``` - Numeral-only simp rules: Replace each rule having a "number_of v" ``` huffman@47108 ` 1212` ``` pattern with two copies, one for numeral and one for neg_numeral. ``` huffman@47108 ` 1213` huffman@47108 ` 1214` ``` - Theorems about subclasses of semiring_1 or ring_1: These classes ``` huffman@47108 ` 1215` ``` automatically support numerals now, so more simp rules and ``` huffman@47108 ` 1216` ``` simprocs may now apply within the proof. ``` huffman@47108 ` 1217` huffman@47108 ` 1218` ``` - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: ``` huffman@47108 ` 1219` ``` Redefine using other integer operations. ``` huffman@47108 ` 1220` wenzelm@47855 ` 1221` ```* Transfer: New package intended to generalize the existing ``` wenzelm@47855 ` 1222` ```"descending" method and related theorem attributes from the Quotient ``` wenzelm@47855 ` 1223` ```package. (Not all functionality is implemented yet, but future ``` wenzelm@47855 ` 1224` ```development will focus on Transfer as an eventual replacement for the ``` wenzelm@47855 ` 1225` ```corresponding parts of the Quotient package.) ``` wenzelm@47809 ` 1226` wenzelm@47809 ` 1227` ``` - transfer_rule attribute: Maintains a collection of transfer rules, ``` wenzelm@47809 ` 1228` ``` which relate constants at two different types. Transfer rules may ``` wenzelm@47809 ` 1229` ``` relate different type instances of the same polymorphic constant, ``` wenzelm@47809 ` 1230` ``` or they may relate an operation on a raw type to a corresponding ``` wenzelm@47809 ` 1231` ``` operation on an abstract type (quotient or subtype). For example: ``` wenzelm@47809 ` 1232` wenzelm@47809 ` 1233` ``` ((A ===> B) ===> list_all2 A ===> list_all2 B) map map ``` wenzelm@47809 ` 1234` ``` (cr_int ===> cr_int ===> cr_int) (%(x,y) (u,v). (x+u, y+v)) plus_int ``` wenzelm@47809 ` 1235` wenzelm@47809 ` 1236` ``` - transfer method: Replaces a subgoal on abstract types with an ``` wenzelm@47809 ` 1237` ``` equivalent subgoal on the corresponding raw types. Constants are ``` wenzelm@47809 ` 1238` ``` replaced with corresponding ones according to the transfer rules. ``` wenzelm@47809 ` 1239` ``` Goals are generalized over all free variables by default; this is ``` huffman@47851 ` 1240` ``` necessary for variables whose types change, but can be overridden ``` wenzelm@47855 ` 1241` ``` for specific variables with e.g. "transfer fixing: x y z". The ``` wenzelm@47809 ` 1242` ``` variant transfer' method allows replacing a subgoal with one that ``` wenzelm@47809 ` 1243` ``` is logically stronger (rather than equivalent). ``` wenzelm@47809 ` 1244` wenzelm@47809 ` 1245` ``` - relator_eq attribute: Collects identity laws for relators of ``` wenzelm@47809 ` 1246` ``` various type constructors, e.g. "list_all2 (op =) = (op =)". The ``` wenzelm@47809 ` 1247` ``` transfer method uses these lemmas to infer transfer rules for ``` wenzelm@47809 ` 1248` ``` non-polymorphic constants on the fly. ``` wenzelm@47809 ` 1249` wenzelm@47809 ` 1250` ``` - transfer_prover method: Assists with proving a transfer rule for a ``` wenzelm@47809 ` 1251` ``` new constant, provided the constant is defined in terms of other ``` wenzelm@47809 ` 1252` ``` constants that already have transfer rules. It should be applied ``` wenzelm@47809 ` 1253` ``` after unfolding the constant definitions. ``` wenzelm@47809 ` 1254` wenzelm@47809 ` 1255` ``` - HOL/ex/Transfer_Int_Nat.thy: Example theory demonstrating transfer ``` wenzelm@47809 ` 1256` ``` from type nat to type int. ``` wenzelm@47809 ` 1257` huffman@47851 ` 1258` ```* Lifting: New package intended to generalize the quotient_definition ``` huffman@47851 ` 1259` ```facility of the Quotient package; designed to work with Transfer. ``` wenzelm@47809 ` 1260` wenzelm@47809 ` 1261` ``` - lift_definition command: Defines operations on an abstract type in ``` wenzelm@47809 ` 1262` ``` terms of a corresponding operation on a representation ``` wenzelm@47809 ` 1263` ``` type. Example syntax: ``` wenzelm@47809 ` 1264` wenzelm@47809 ` 1265` ``` lift_definition dlist_insert :: "'a => 'a dlist => 'a dlist" ``` wenzelm@47809 ` 1266` ``` is List.insert ``` wenzelm@47809 ` 1267` wenzelm@47809 ` 1268` ``` Users must discharge a respectfulness proof obligation when each ``` wenzelm@47809 ` 1269` ``` constant is defined. (For a type copy, i.e. a typedef with UNIV, ``` wenzelm@47809 ` 1270` ``` the proof is discharged automatically.) The obligation is ``` wenzelm@47809 ` 1271` ``` presented in a user-friendly, readable form; a respectfulness ``` wenzelm@47809 ` 1272` ``` theorem in the standard format and a transfer rule are generated ``` wenzelm@47809 ` 1273` ``` by the package. ``` wenzelm@47809 ` 1274` wenzelm@47809 ` 1275` ``` - Integration with code_abstype: For typedefs (e.g. subtypes ``` wenzelm@47809 ` 1276` ``` corresponding to a datatype invariant, such as dlist), ``` wenzelm@47809 ` 1277` ``` lift_definition generates a code certificate theorem and sets up ``` wenzelm@47809 ` 1278` ``` code generation for each constant. ``` wenzelm@47809 ` 1279` wenzelm@47809 ` 1280` ``` - setup_lifting command: Sets up the Lifting package to work with a ``` wenzelm@47809 ` 1281` ``` user-defined type. The user must provide either a quotient theorem ``` wenzelm@47809 ` 1282` ``` or a type_definition theorem. The package configures transfer ``` wenzelm@47809 ` 1283` ``` rules for equality and quantifiers on the type, and sets up the ``` wenzelm@47809 ` 1284` ``` lift_definition command to work with the type. ``` wenzelm@47809 ` 1285` wenzelm@47809 ` 1286` ``` - Usage examples: See Quotient_Examples/Lift_DList.thy, ``` huffman@47851 ` 1287` ``` Quotient_Examples/Lift_RBT.thy, Quotient_Examples/Lift_FSet.thy, ``` huffman@47851 ` 1288` ``` Word/Word.thy and Library/Float.thy. ``` wenzelm@47809 ` 1289` wenzelm@47809 ` 1290` ```* Quotient package: ``` wenzelm@47809 ` 1291` wenzelm@47809 ` 1292` ``` - The 'quotient_type' command now supports a 'morphisms' option with ``` wenzelm@47809 ` 1293` ``` rep and abs functions, similar to typedef. ``` wenzelm@47809 ` 1294` wenzelm@47809 ` 1295` ``` - 'quotient_type' sets up new types to work with the Lifting and ``` wenzelm@47809 ` 1296` ``` Transfer packages, as with 'setup_lifting'. ``` wenzelm@47809 ` 1297` wenzelm@47809 ` 1298` ``` - The 'quotient_definition' command now requires the user to prove a ``` wenzelm@47809 ` 1299` ``` respectfulness property at the point where the constant is ``` wenzelm@47809 ` 1300` ``` defined, similar to lift_definition; INCOMPATIBILITY. ``` wenzelm@47809 ` 1301` wenzelm@47809 ` 1302` ``` - Renamed predicate 'Quotient' to 'Quotient3', and renamed theorems ``` wenzelm@47809 ` 1303` ``` accordingly, INCOMPATIBILITY. ``` wenzelm@47809 ` 1304` wenzelm@47809 ` 1305` ```* New diagnostic command 'find_unused_assms' to find potentially ``` wenzelm@47809 ` 1306` ```superfluous assumptions in theorems using Quickcheck. ``` wenzelm@47809 ` 1307` wenzelm@47809 ` 1308` ```* Quickcheck: ``` wenzelm@47809 ` 1309` wenzelm@47809 ` 1310` ``` - Quickcheck returns variable assignments as counterexamples, which ``` wenzelm@47809 ` 1311` ``` allows to reveal the underspecification of functions under test. ``` wenzelm@47809 ` 1312` ``` For example, refuting "hd xs = x", it presents the variable ``` wenzelm@47809 ` 1313` ``` assignment xs = [] and x = a1 as a counterexample, assuming that ``` wenzelm@47809 ` 1314` ``` any property is false whenever "hd []" occurs in it. ``` wenzelm@47809 ` 1315` wenzelm@47809 ` 1316` ``` These counterexample are marked as potentially spurious, as ``` wenzelm@47809 ` 1317` ``` Quickcheck also returns "xs = []" as a counterexample to the ``` wenzelm@47809 ` 1318` ``` obvious theorem "hd xs = hd xs". ``` wenzelm@47809 ` 1319` wenzelm@47809 ` 1320` ``` After finding a potentially spurious counterexample, Quickcheck ``` wenzelm@47809 ` 1321` ``` continues searching for genuine ones. ``` wenzelm@47809 ` 1322` wenzelm@47809 ` 1323` ``` By default, Quickcheck shows potentially spurious and genuine ``` wenzelm@47809 ` 1324` ``` counterexamples. The option "genuine_only" sets quickcheck to only ``` wenzelm@47809 ` 1325` ``` show genuine counterexamples. ``` wenzelm@47809 ` 1326` wenzelm@47809 ` 1327` ``` - The command 'quickcheck_generator' creates random and exhaustive ``` wenzelm@47809 ` 1328` ``` value generators for a given type and operations. ``` wenzelm@47809 ` 1329` wenzelm@47809 ` 1330` ``` It generates values by using the operations as if they were ``` wenzelm@47809 ` 1331` ``` constructors of that type. ``` wenzelm@47809 ` 1332` wenzelm@47809 ` 1333` ``` - Support for multisets. ``` wenzelm@47809 ` 1334` wenzelm@47809 ` 1335` ``` - Added "use_subtype" options. ``` wenzelm@47809 ` 1336` wenzelm@47809 ` 1337` ``` - Added "quickcheck_locale" configuration to specify how to process ``` wenzelm@47809 ` 1338` ``` conjectures in a locale context. ``` wenzelm@47809 ` 1339` wenzelm@47855 ` 1340` ```* Nitpick: Fixed infinite loop caused by the 'peephole_optim' option ``` wenzelm@47855 ` 1341` ```and affecting 'rat' and 'real'. ``` wenzelm@47809 ` 1342` wenzelm@47809 ` 1343` ```* Sledgehammer: ``` wenzelm@47809 ` 1344` ``` - Integrated more tightly with SPASS, as described in the ITP 2012 ``` wenzelm@47809 ` 1345` ``` paper "More SPASS with Isabelle". ``` wenzelm@47809 ` 1346` ``` - Made it try "smt" as a fallback if "metis" fails or times out. ``` wenzelm@47809 ` 1347` ``` - Added support for the following provers: Alt-Ergo (via Why3 and ``` wenzelm@47809 ` 1348` ``` TFF1), iProver, iProver-Eq. ``` wenzelm@47809 ` 1349` ``` - Sped up the minimizer. ``` wenzelm@47809 ` 1350` ``` - Added "lam_trans", "uncurry_aliases", and "minimize" options. ``` wenzelm@47809 ` 1351` ``` - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice"). ``` wenzelm@47809 ` 1352` ``` - Renamed "sound" option to "strict". ``` wenzelm@47809 ` 1353` wenzelm@47855 ` 1354` ```* Metis: Added possibility to specify lambda translations scheme as a ``` wenzelm@47855 ` 1355` ```parenthesized argument (e.g., "by (metis (lifting) ...)"). ``` wenzelm@47855 ` 1356` wenzelm@47855 ` 1357` ```* SMT: Renamed "smt_fixed" option to "smt_read_only_certificates". ``` wenzelm@47855 ` 1358` wenzelm@47855 ` 1359` ```* Command 'try0': Renamed from 'try_methods'. INCOMPATIBILITY. ``` wenzelm@47809 ` 1360` wenzelm@47856 ` 1361` ```* New "case_product" attribute to generate a case rule doing multiple ``` wenzelm@47856 ` 1362` ```case distinctions at the same time. E.g. ``` wenzelm@47856 ` 1363` wenzelm@47856 ` 1364` ``` list.exhaust [case_product nat.exhaust] ``` wenzelm@47856 ` 1365` wenzelm@47856 ` 1366` ```produces a rule which can be used to perform case distinction on both ``` wenzelm@47856 ` 1367` ```a list and a nat. ``` wenzelm@47856 ` 1368` wenzelm@47809 ` 1369` ```* New "eventually_elim" method as a generalized variant of the ``` wenzelm@47855 ` 1370` ```eventually_elim* rules. Supports structured proofs. ``` wenzelm@47855 ` 1371` wenzelm@47702 ` 1372` ```* Typedef with implicit set definition is considered legacy. Use ``` wenzelm@47702 ` 1373` ```"typedef (open)" form instead, which will eventually become the ``` wenzelm@47702 ` 1374` ```default. ``` wenzelm@47702 ` 1375` wenzelm@47856 ` 1376` ```* Record: code generation can be switched off manually with ``` wenzelm@47856 ` 1377` wenzelm@47856 ` 1378` ``` declare [[record_coden = false]] -- "default true" ``` wenzelm@47856 ` 1379` wenzelm@47856 ` 1380` ```* Datatype: type parameters allow explicit sort constraints. ``` wenzelm@47856 ` 1381` wenzelm@47855 ` 1382` ```* Concrete syntax for case expressions includes constraints for source ``` wenzelm@47855 ` 1383` ```positions, and thus produces Prover IDE markup for its bindings. ``` wenzelm@47855 ` 1384` ```INCOMPATIBILITY for old-style syntax translations that augment the ``` wenzelm@47855 ` 1385` ```pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of ``` wenzelm@47855 ` 1386` ```one_case. ``` wenzelm@47855 ` 1387` wenzelm@47855 ` 1388` ```* Clarified attribute "mono_set": pure declaration without modifying ``` wenzelm@47855 ` 1389` ```the result of the fact expression. ``` wenzelm@47855 ` 1390` haftmann@46752 ` 1391` ```* More default pred/set conversions on a couple of relation operations ``` wenzelm@47464 ` 1392` ```and predicates. Added powers of predicate relations. Consolidation ``` wenzelm@47464 ` 1393` ```of some relation theorems: ``` haftmann@46752 ` 1394` haftmann@46752 ` 1395` ``` converse_def ~> converse_unfold ``` haftmann@47549 ` 1396` ``` rel_comp_def ~> relcomp_unfold ``` haftmann@47820 ` 1397` ``` symp_def ~> (modified, use symp_def and sym_def instead) ``` haftmann@46752 ` 1398` ``` transp_def ~> transp_trans ``` haftmann@46752 ` 1399` ``` Domain_def ~> Domain_unfold ``` haftmann@46752 ` 1400` ``` Range_def ~> Domain_converse [symmetric] ``` haftmann@46752 ` 1401` haftmann@46981 ` 1402` ```Generalized theorems INF_INT_eq, INF_INT_eq2, SUP_UN_eq, SUP_UN_eq2. ``` haftmann@46981 ` 1403` wenzelm@47464 ` 1404` ```See theory "Relation" for examples for making use of pred/set ``` wenzelm@47464 ` 1405` ```conversions by means of attributes "to_set" and "to_pred". ``` haftmann@47086 ` 1406` haftmann@46752 ` 1407` ```INCOMPATIBILITY. ``` haftmann@46752 ` 1408` bulwahn@46363 ` 1409` ```* Renamed facts about the power operation on relations, i.e., relpow ``` wenzelm@47464 ` 1410` ```to match the constant's name: ``` wenzelm@47463 ` 1411` wenzelm@46458 ` 1412` ``` rel_pow_1 ~> relpow_1 ``` bulwahn@46363 ` 1413` ``` rel_pow_0_I ~> relpow_0_I ``` bulwahn@46363 ` 1414` ``` rel_pow_Suc_I ~> relpow_Suc_I ``` bulwahn@46363 ` 1415` ``` rel_pow_Suc_I2 ~> relpow_Suc_I2 ``` bulwahn@46363 ` 1416` ``` rel_pow_0_E ~> relpow_0_E ``` bulwahn@46363 ` 1417` ``` rel_pow_Suc_E ~> relpow_Suc_E ``` bulwahn@46363 ` 1418` ``` rel_pow_E ~> relpow_E ``` wenzelm@46458 ` 1419` ``` rel_pow_Suc_D2 ~> relpow_Suc_D2 ``` wenzelm@47463 ` 1420` ``` rel_pow_Suc_E2 ~> relpow_Suc_E2 ``` bulwahn@46363 ` 1421` ``` rel_pow_Suc_D2' ~> relpow_Suc_D2' ``` bulwahn@46363 ` 1422` ``` rel_pow_E2 ~> relpow_E2 ``` bulwahn@46363 ` 1423` ``` rel_pow_add ~> relpow_add ``` bulwahn@46363 ` 1424` ``` rel_pow_commute ~> relpow ``` bulwahn@46363 ` 1425` ``` rel_pow_empty ~> relpow_empty: ``` bulwahn@46363 ` 1426` ``` rtrancl_imp_UN_rel_pow ~> rtrancl_imp_UN_relpow ``` bulwahn@46363 ` 1427` ``` rel_pow_imp_rtrancl ~> relpow_imp_rtrancl ``` bulwahn@46363 ` 1428` ``` rtrancl_is_UN_rel_pow ~> rtrancl_is_UN_relpow ``` bulwahn@46363 ` 1429` ``` rtrancl_imp_rel_pow ~> rtrancl_imp_relpow ``` bulwahn@46363 ` 1430` ``` rel_pow_fun_conv ~> relpow_fun_conv ``` bulwahn@46363 ` 1431` ``` rel_pow_finite_bounded1 ~> relpow_finite_bounded1 ``` bulwahn@46363 ` 1432` ``` rel_pow_finite_bounded ~> relpow_finite_bounded ``` bulwahn@46363 ` 1433` ``` rtrancl_finite_eq_rel_pow ~> rtrancl_finite_eq_relpow ``` bulwahn@46363 ` 1434` ``` trancl_finite_eq_rel_pow ~> trancl_finite_eq_relpow ``` bulwahn@46363 ` 1435` ``` single_valued_rel_pow ~> single_valued_relpow ``` wenzelm@47463 ` 1436` bulwahn@46363 ` 1437` ```INCOMPATIBILITY. ``` bulwahn@46363 ` 1438` bulwahn@47448 ` 1439` ```* Theory Relation: Consolidated constant name for relation composition ``` wenzelm@47464 ` 1440` ```and corresponding theorem names: ``` wenzelm@47464 ` 1441` haftmann@47549 ` 1442` ``` - Renamed constant rel_comp to relcomp. ``` wenzelm@47464 ` 1443` bulwahn@47448 ` 1444` ``` - Dropped abbreviation pred_comp. Use relcompp instead. ``` wenzelm@47464 ` 1445` bulwahn@47448 ` 1446` ``` - Renamed theorems: ``` wenzelm@47464 ` 1447` bulwahn@47448 ` 1448` ``` rel_compI ~> relcompI ``` bulwahn@47448 ` 1449` ``` rel_compEpair ~> relcompEpair ``` bulwahn@47448 ` 1450` ``` rel_compE ~> relcompE ``` bulwahn@47448 ` 1451` ``` pred_comp_rel_comp_eq ~> relcompp_relcomp_eq ``` bulwahn@47448 ` 1452` ``` rel_comp_empty1 ~> relcomp_empty1 ``` bulwahn@47448 ` 1453` ``` rel_comp_mono ~> relcomp_mono ``` bulwahn@47448 ` 1454` ``` rel_comp_subset_Sigma ~> relcomp_subset_Sigma ``` bulwahn@47448 ` 1455` ``` rel_comp_distrib ~> relcomp_distrib ``` bulwahn@47448 ` 1456` ``` rel_comp_distrib2 ~> relcomp_distrib2 ``` bulwahn@47448 ` 1457` ``` rel_comp_UNION_distrib ~> relcomp_UNION_distrib ``` bulwahn@47448 ` 1458` ``` rel_comp_UNION_distrib2 ~> relcomp_UNION_distrib2 ``` bulwahn@47448 ` 1459` ``` single_valued_rel_comp ~> single_valued_relcomp ``` haftmann@47549 ` 1460` ``` rel_comp_def ~> relcomp_unfold ``` bulwahn@47448 ` 1461` ``` converse_rel_comp ~> converse_relcomp ``` bulwahn@47448 ` 1462` ``` pred_compI ~> relcomppI ``` bulwahn@47448 ` 1463` ``` pred_compE ~> relcomppE ``` bulwahn@47448 ` 1464` ``` pred_comp_bot1 ~> relcompp_bot1 ``` bulwahn@47448 ` 1465` ``` pred_comp_bot2 ~> relcompp_bot2 ``` bulwahn@47448 ` 1466` ``` transp_pred_comp_less_eq ~> transp_relcompp_less_eq ``` bulwahn@47448 ` 1467` ``` pred_comp_mono ~> relcompp_mono ``` bulwahn@47448 ` 1468` ``` pred_comp_distrib ~> relcompp_distrib ``` bulwahn@47448 ` 1469` ``` pred_comp_distrib2 ~> relcompp_distrib2 ``` bulwahn@47448 ` 1470` ``` converse_pred_comp ~> converse_relcompp ``` wenzelm@47464 ` 1471` bulwahn@47448 ` 1472` ``` finite_rel_comp ~> finite_relcomp ``` wenzelm@47464 ` 1473` bulwahn@47448 ` 1474` ``` set_rel_comp ~> set_relcomp ``` bulwahn@47448 ` 1475` bulwahn@47448 ` 1476` ```INCOMPATIBILITY. ``` bulwahn@47448 ` 1477` haftmann@47550 ` 1478` ```* Theory Divides: Discontinued redundant theorems about div and mod. ``` haftmann@47550 ` 1479` ```INCOMPATIBILITY, use the corresponding generic theorems instead. ``` haftmann@47550 ` 1480` haftmann@47550 ` 1481` ``` DIVISION_BY_ZERO ~> div_by_0, mod_by_0 ``` haftmann@47550 ` 1482` ``` zdiv_self ~> div_self ``` haftmann@47550 ` 1483` ``` zmod_self ~> mod_self ``` haftmann@47550 ` 1484` ``` zdiv_zero ~> div_0 ``` haftmann@47550 ` 1485` ``` zmod_zero ~> mod_0 ``` haftmann@47550 ` 1486` ``` zdiv_zmod_equality ~> div_mod_equality2 ``` haftmann@47550 ` 1487` ``` zdiv_zmod_equality2 ~> div_mod_equality ``` haftmann@47550 ` 1488` ``` zmod_zdiv_trivial ~> mod_div_trivial ``` haftmann@47550 ` 1489` ``` zdiv_zminus_zminus ~> div_minus_minus ``` haftmann@47550 ` 1490` ``` zmod_zminus_zminus ~> mod_minus_minus ``` haftmann@47550 ` 1491` ``` zdiv_zminus2 ~> div_minus_right ``` haftmann@47550 ` 1492` ``` zmod_zminus2 ~> mod_minus_right ``` haftmann@47550 ` 1493` ``` zdiv_minus1_right ~> div_minus1_right ``` haftmann@47550 ` 1494` ``` zmod_minus1_right ~> mod_minus1_right ``` haftmann@47550 ` 1495` ``` zdvd_mult_div_cancel ~> dvd_mult_div_cancel ``` haftmann@47550 ` 1496` ``` zmod_zmult1_eq ~> mod_mult_right_eq ``` haftmann@47550 ` 1497` ``` zpower_zmod ~> power_mod ``` haftmann@47550 ` 1498` ``` zdvd_zmod ~> dvd_mod ``` haftmann@47550 ` 1499` ``` zdvd_zmod_imp_zdvd ~> dvd_mod_imp_dvd ``` haftmann@47550 ` 1500` ``` mod_mult_distrib ~> mult_mod_left ``` haftmann@47550 ` 1501` ``` mod_mult_distrib2 ~> mult_mod_right ``` haftmann@47550 ` 1502` haftmann@47550 ` 1503` ```* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use ``` haftmann@47550 ` 1504` ```generic mult_2 and mult_2_right instead. INCOMPATIBILITY. ``` haftmann@47550 ` 1505` haftmann@47551 ` 1506` ```* Finite_Set.fold now qualified. INCOMPATIBILITY. ``` haftmann@47551 ` 1507` haftmann@47552 ` 1508` ```* Consolidated theorem names concerning fold combinators: ``` haftmann@47550 ` 1509` haftmann@47550 ` 1510` ``` inf_INFI_fold_inf ~> inf_INF_fold_inf ``` haftmann@47550 ` 1511` ``` sup_SUPR_fold_sup ~> sup_SUP_fold_sup ``` haftmann@47550 ` 1512` ``` INFI_fold_inf ~> INF_fold_inf ``` haftmann@47550 ` 1513` ``` SUPR_fold_sup ~> SUP_fold_sup ``` haftmann@47550 ` 1514` ``` union_set ~> union_set_fold ``` haftmann@47550 ` 1515` ``` minus_set ~> minus_set_fold ``` haftmann@47550 ` 1516` ``` INFI_set_fold ~> INF_set_fold ``` haftmann@47550 ` 1517` ``` SUPR_set_fold ~> SUP_set_fold ``` haftmann@47550 ` 1518` ``` INF_code ~> INF_set_foldr ``` haftmann@47550 ` 1519` ``` SUP_code ~> SUP_set_foldr ``` haftmann@47550 ` 1520` ``` foldr.simps ~> foldr.simps (in point-free formulation) ``` haftmann@47550 ` 1521` ``` foldr_fold_rev ~> foldr_conv_fold ``` haftmann@47550 ` 1522` ``` foldl_fold ~> foldl_conv_fold ``` haftmann@47550 ` 1523` ``` foldr_foldr ~> foldr_conv_foldl ``` haftmann@47550 ` 1524` ``` foldl_foldr ~> foldl_conv_foldr ``` haftmann@47552 ` 1525` ``` fold_set_remdups ~> fold_set_fold_remdups ``` haftmann@47552 ` 1526` ``` fold_set ~> fold_set_fold ``` haftmann@47552 ` 1527` ``` fold1_set ~> fold1_set_fold ``` haftmann@47550 ` 1528` haftmann@47550 ` 1529` ```INCOMPATIBILITY. ``` haftmann@47550 ` 1530` haftmann@47550 ` 1531` ```* Dropped rarely useful theorems concerning fold combinators: ``` haftmann@47550 ` 1532` ```foldl_apply, foldl_fun_comm, foldl_rev, fold_weak_invariant, ``` haftmann@47550 ` 1533` ```rev_foldl_cons, fold_set_remdups, fold_set, fold_set1, ``` haftmann@47550 ` 1534` ```concat_conv_foldl, foldl_weak_invariant, foldl_invariant, ``` haftmann@47550 ` 1535` ```foldr_invariant, foldl_absorb0, foldl_foldr1_lemma, foldl_foldr1, ``` haftmann@47550 ` 1536` ```listsum_conv_fold, listsum_foldl, sort_foldl_insort, foldl_assoc, ``` haftmann@47550 ` 1537` ```foldr_conv_foldl, start_le_sum, elem_le_sum, sum_eq_0_conv. ``` haftmann@47550 ` 1538` ```INCOMPATIBILITY. For the common phrases "%xs. List.foldr plus xs 0" ``` haftmann@47550 ` 1539` ```and "List.foldl plus 0", prefer "List.listsum". Otherwise it can be ``` haftmann@47550 ` 1540` ```useful to boil down "List.foldr" and "List.foldl" to "List.fold" by ``` haftmann@47550 ` 1541` ```unfolding "foldr_conv_fold" and "foldl_conv_fold". ``` haftmann@47550 ` 1542` haftmann@47550 ` 1543` ```* Dropped lemmas minus_set_foldr, union_set_foldr, union_coset_foldr, ``` haftmann@47550 ` 1544` ```inter_coset_foldr, Inf_fin_set_foldr, Sup_fin_set_foldr, ``` haftmann@47550 ` 1545` ```Min_fin_set_foldr, Max_fin_set_foldr, Inf_set_foldr, Sup_set_foldr, ``` haftmann@47550 ` 1546` ```INF_set_foldr, SUP_set_foldr. INCOMPATIBILITY. Prefer corresponding ``` haftmann@47550 ` 1547` ```lemmas over fold rather than foldr, or make use of lemmas ``` haftmann@47550 ` 1548` ```fold_conv_foldr and fold_rev. ``` haftmann@47550 ` 1549` haftmann@47550 ` 1550` ```* Congruence rules Option.map_cong and Option.bind_cong for recursion ``` haftmann@47550 ` 1551` ```through option types. ``` haftmann@47550 ` 1552` wenzelm@47856 ` 1553` ```* "Transitive_Closure.ntrancl": bounded transitive closure on ``` wenzelm@47856 ` 1554` ```relations. ``` wenzelm@47856 ` 1555` wenzelm@47856 ` 1556` ```* Constant "Set.not_member" now qualified. INCOMPATIBILITY. ``` wenzelm@47856 ` 1557` wenzelm@47856 ` 1558` ```* Theory Int: Discontinued many legacy theorems specific to type int. ``` wenzelm@47856 ` 1559` ```INCOMPATIBILITY, use the corresponding generic theorems instead. ``` wenzelm@47856 ` 1560` wenzelm@47856 ` 1561` ``` zminus_zminus ~> minus_minus ``` wenzelm@47856 ` 1562` ``` zminus_0 ~> minus_zero ``` wenzelm@47856 ` 1563` ``` zminus_zadd_distrib ~> minus_add_distrib ``` wenzelm@47856 ` 1564` ``` zadd_commute ~> add_commute ``` wenzelm@47856 ` 1565` ``` zadd_assoc ~> add_assoc ``` wenzelm@47856 ` 1566` ``` zadd_left_commute ~> add_left_commute ``` wenzelm@47856 ` 1567` ``` zadd_ac ~> add_ac ``` wenzelm@47856 ` 1568` ``` zmult_ac ~> mult_ac ``` wenzelm@47856 ` 1569` ``` zadd_0 ~> add_0_left ``` wenzelm@47856 ` 1570` ``` zadd_0_right ~> add_0_right ``` wenzelm@47856 ` 1571` ``` zadd_zminus_inverse2 ~> left_minus ``` wenzelm@47856 ` 1572` ``` zmult_zminus ~> mult_minus_left ``` wenzelm@47856 ` 1573` ``` zmult_commute ~> mult_commute ``` wenzelm@47856 ` 1574` ``` zmult_assoc ~> mult_assoc ``` wenzelm@47856 ` 1575` ``` zadd_zmult_distrib ~> left_distrib ``` wenzelm@47856 ` 1576` ``` zadd_zmult_distrib2 ~> right_distrib ``` wenzelm@47856 ` 1577` ``` zdiff_zmult_distrib ~> left_diff_distrib ``` wenzelm@47856 ` 1578` ``` zdiff_zmult_distrib2 ~> right_diff_distrib ``` wenzelm@47856 ` 1579` ``` zmult_1 ~> mult_1_left ``` wenzelm@47856 ` 1580` ``` zmult_1_right ~> mult_1_right ``` wenzelm@47856 ` 1581` ``` zle_refl ~> order_refl ``` wenzelm@47856 ` 1582` ``` zle_trans ~> order_trans ``` wenzelm@47856 ` 1583` ``` zle_antisym ~> order_antisym ``` wenzelm@47856 ` 1584` ``` zle_linear ~> linorder_linear ``` wenzelm@47856 ` 1585` ``` zless_linear ~> linorder_less_linear ``` wenzelm@47856 ` 1586` ``` zadd_left_mono ~> add_left_mono ``` wenzelm@47856 ` 1587` ``` zadd_strict_right_mono ~> add_strict_right_mono ``` wenzelm@47856 ` 1588` ``` zadd_zless_mono ~> add_less_le_mono ``` wenzelm@47856 ` 1589` ``` int_0_less_1 ~> zero_less_one ``` wenzelm@47856 ` 1590` ``` int_0_neq_1 ~> zero_neq_one ``` wenzelm@47856 ` 1591` ``` zless_le ~> less_le ``` wenzelm@47856 ` 1592` ``` zpower_zadd_distrib ~> power_add ``` wenzelm@47856 ` 1593` ``` zero_less_zpower_abs_iff ~> zero_less_power_abs_iff ``` wenzelm@47856 ` 1594` ``` zero_le_zpower_abs ~> zero_le_power_abs ``` wenzelm@47856 ` 1595` wenzelm@47856 ` 1596` ```* Theory Deriv: Renamed ``` wenzelm@47856 ` 1597` wenzelm@47856 ` 1598` ``` DERIV_nonneg_imp_nonincreasing ~> DERIV_nonneg_imp_nondecreasing ``` wenzelm@47856 ` 1599` wenzelm@47856 ` 1600` ```* Theory Library/Multiset: Improved code generation of multisets. ``` wenzelm@47856 ` 1601` wenzelm@47855 ` 1602` ```* Theory HOL/Library/Set_Algebras: Addition and multiplication on sets ``` krauss@47703 ` 1603` ```are expressed via type classes again. The special syntax ``` krauss@47703 ` 1604` ```\/\ has been replaced by plain +/*. Removed constant ``` krauss@47703 ` 1605` ```setsum_set, which is now subsumed by Big_Operators.setsum. ``` krauss@47703 ` 1606` ```INCOMPATIBILITY. ``` krauss@47703 ` 1607` wenzelm@46160 ` 1608` ```* Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, ``` wenzelm@46160 ` 1609` ```use theory HOL/Library/Nat_Bijection instead. ``` wenzelm@46160 ` 1610` wenzelm@47464 ` 1611` ```* Theory HOL/Library/RBT_Impl: Backing implementation of red-black ``` wenzelm@47464 ` 1612` ```trees is now inside a type class context. Names of affected ``` wenzelm@47464 ` 1613` ```operations and lemmas have been prefixed by rbt_. INCOMPATIBILITY for ``` wenzelm@47464 ` 1614` ```theories working directly with raw red-black trees, adapt the names as ``` wenzelm@47464 ` 1615` ```follows: ``` Andreas@47452 ` 1616` Andreas@47452 ` 1617` ``` Operations: ``` Andreas@47452 ` 1618` ``` bulkload -> rbt_bulkload ``` Andreas@47452 ` 1619` ``` del_from_left -> rbt_del_from_left ``` Andreas@47452 ` 1620` ``` del_from_right -> rbt_del_from_right ``` Andreas@47452 ` 1621` ``` del -> rbt_del ``` Andreas@47452 ` 1622` ``` delete -> rbt_delete ``` Andreas@47452 ` 1623` ``` ins -> rbt_ins ``` Andreas@47452 ` 1624` ``` insert -> rbt_insert ``` Andreas@47452 ` 1625` ``` insertw -> rbt_insert_with ``` Andreas@47452 ` 1626` ``` insert_with_key -> rbt_insert_with_key ``` Andreas@47452 ` 1627` ``` map_entry -> rbt_map_entry ``` Andreas@47452 ` 1628` ``` lookup -> rbt_lookup ``` Andreas@47452 ` 1629` ``` sorted -> rbt_sorted ``` Andreas@47452 ` 1630` ``` tree_greater -> rbt_greater ``` Andreas@47452 ` 1631` ``` tree_less -> rbt_less ``` Andreas@47452 ` 1632` ``` tree_less_symbol -> rbt_less_symbol ``` Andreas@47452 ` 1633` ``` union -> rbt_union ``` Andreas@47452 ` 1634` ``` union_with -> rbt_union_with ``` Andreas@47452 ` 1635` ``` union_with_key -> rbt_union_with_key ``` Andreas@47452 ` 1636` Andreas@47452 ` 1637` ``` Lemmas: ``` Andreas@47452 ` 1638` ``` balance_left_sorted -> balance_left_rbt_sorted ``` Andreas@47452 ` 1639` ``` balance_left_tree_greater -> balance_left_rbt_greater ``` Andreas@47452 ` 1640` ``` balance_left_tree_less -> balance_left_rbt_less ``` Andreas@47452 ` 1641` ``` balance_right_sorted -> balance_right_rbt_sorted ``` Andreas@47452 ` 1642` ``` balance_right_tree_greater -> balance_right_rbt_greater ``` Andreas@47452 ` 1643` ``` balance_right_tree_less -> balance_right_rbt_less ``` Andreas@47452 ` 1644` ``` balance_sorted -> balance_rbt_sorted ``` Andreas@47452 ` 1645` ``` balance_tree_greater -> balance_rbt_greater ``` Andreas@47452 ` 1646` ``` balance_tree_less -> balance_rbt_less ``` Andreas@47452 ` 1647` ``` bulkload_is_rbt -> rbt_bulkload_is_rbt ``` Andreas@47452 ` 1648` ``` combine_sorted -> combine_rbt_sorted ``` Andreas@47452 ` 1649` ``` combine_tree_greater -> combine_rbt_greater ``` Andreas@47452 ` 1650` ``` combine_tree_less -> combine_rbt_less ``` Andreas@47452 ` 1651` ``` delete_in_tree -> rbt_delete_in_tree ``` Andreas@47452 ` 1652` ``` delete_is_rbt -> rbt_delete_is_rbt ``` Andreas@47452 ` 1653` ``` del_from_left_tree_greater -> rbt_del_from_left_rbt_greater ``` Andreas@47452 ` 1654` ``` del_from_left_tree_less -> rbt_del_from_left_rbt_less ``` Andreas@47452 ` 1655` ``` del_from_right_tree_greater -> rbt_del_from_right_rbt_greater ``` Andreas@47452 ` 1656` ``` del_from_right_tree_less -> rbt_del_from_right_rbt_less ``` Andreas@47452 ` 1657` ``` del_in_tree -> rbt_del_in_tree ``` Andreas@47452 ` 1658` ``` del_inv1_inv2 -> rbt_del_inv1_inv2 ``` Andreas@47452 ` 1659` ``` del_sorted -> rbt_del_rbt_sorted ``` Andreas@47452 ` 1660` ``` del_tree_greater -> rbt_del_rbt_greater ``` Andreas@47452 ` 1661` ``` del_tree_less -> rbt_del_rbt_less ``` Andreas@47452 ` 1662` ``` dom_lookup_Branch -> dom_rbt_lookup_Branch ``` Andreas@47452 ` 1663` ``` entries_lookup -> entries_rbt_lookup ``` Andreas@47452 ` 1664` ``` finite_dom_lookup -> finite_dom_rbt_lookup ``` Andreas@47452 ` 1665` ``` insert_sorted -> rbt_insert_rbt_sorted ``` Andreas@47452 ` 1666` ``` insertw_is_rbt -> rbt_insertw_is_rbt ``` Andreas@47452 ` 1667` ``` insertwk_is_rbt -> rbt_insertwk_is_rbt ``` Andreas@47452 ` 1668` ``` insertwk_sorted -> rbt_insertwk_rbt_sorted ``` Andreas@47452 ` 1669` ``` insertw_sorted -> rbt_insertw_rbt_sorted ``` Andreas@47452 ` 1670` ``` ins_sorted -> ins_rbt_sorted ``` Andreas@47452 ` 1671` ``` ins_tree_greater -> ins_rbt_greater ``` Andreas@47452 ` 1672` ``` ins_tree_less -> ins_rbt_less ``` Andreas@47452 ` 1673` ``` is_rbt_sorted -> is_rbt_rbt_sorted ``` Andreas@47452 ` 1674` ``` lookup_balance -> rbt_lookup_balance ``` Andreas@47452 ` 1675` ``` lookup_bulkload -> rbt_lookup_rbt_bulkload ``` Andreas@47452 ` 1676` ``` lookup_delete -> rbt_lookup_rbt_delete ``` Andreas@47452 ` 1677` ``` lookup_Empty -> rbt_lookup_Empty ``` Andreas@47452 ` 1678` ``` lookup_from_in_tree -> rbt_lookup_from_in_tree ``` Andreas@47452 ` 1679` ``` lookup_in_tree -> rbt_lookup_in_tree ``` Andreas@47452 ` 1680` ``` lookup_ins -> rbt_lookup_ins ``` Andreas@47452 ` 1681` ``` lookup_insert -> rbt_lookup_rbt_insert ``` Andreas@47452 ` 1682` ``` lookup_insertw -> rbt_lookup_rbt_insertw ``` Andreas@47452 ` 1683` ``` lookup_insertwk -> rbt_lookup_rbt_insertwk ``` Andreas@47452 ` 1684` ``` lookup_keys -> rbt_lookup_keys ``` Andreas@47452 ` 1685` ``` lookup_map -> rbt_lookup_map ``` Andreas@47452 ` 1686` ``` lookup_map_entry -> rbt_lookup_rbt_map_entry ``` Andreas@47452 ` 1687` ``` lookup_tree_greater -> rbt_lookup_rbt_greater ``` Andreas@47452 ` 1688` ``` lookup_tree_less -> rbt_lookup_rbt_less ``` Andreas@47452 ` 1689` ``` lookup_union -> rbt_lookup_rbt_union ``` Andreas@47452 ` 1690` ``` map_entry_color_of -> rbt_map_entry_color_of ``` Andreas@47452 ` 1691` ``` map_entry_inv1 -> rbt_map_entry_inv1 ``` Andreas@47452 ` 1692` ``` map_entry_inv2 -> rbt_map_entry_inv2 ``` Andreas@47452 ` 1693` ``` map_entry_is_rbt -> rbt_map_entry_is_rbt ``` Andreas@47452 ` 1694` ``` map_entry_sorted -> rbt_map_entry_rbt_sorted ``` Andreas@47452 ` 1695` ``` map_entry_tree_greater -> rbt_map_entry_rbt_greater ``` Andreas@47452 ` 1696` ``` map_entry_tree_less -> rbt_map_entry_rbt_less ``` Andreas@47452 ` 1697` ``` map_tree_greater -> map_rbt_greater ``` Andreas@47452 ` 1698` ``` map_tree_less -> map_rbt_less ``` Andreas@47452 ` 1699` ``` map_sorted -> map_rbt_sorted ``` Andreas@47452 ` 1700` ``` paint_sorted -> paint_rbt_sorted ``` Andreas@47452 ` 1701` ``` paint_lookup -> paint_rbt_lookup ``` Andreas@47452 ` 1702` ``` paint_tree_greater -> paint_rbt_greater ``` Andreas@47452 ` 1703` ``` paint_tree_less -> paint_rbt_less ``` Andreas@47452 ` 1704` ``` sorted_entries -> rbt_sorted_entries ``` Andreas@47452 ` 1705` ``` tree_greater_eq_trans -> rbt_greater_eq_trans ``` Andreas@47452 ` 1706` ``` tree_greater_nit -> rbt_greater_nit ``` Andreas@47452 ` 1707` ``` tree_greater_prop -> rbt_greater_prop ``` Andreas@47452 ` 1708` ``` tree_greater_simps -> rbt_greater_simps ``` Andreas@47452 ` 1709` ``` tree_greater_trans -> rbt_greater_trans ``` Andreas@47452 ` 1710` ``` tree_less_eq_trans -> rbt_less_eq_trans ``` Andreas@47452 ` 1711` ``` tree_less_nit -> rbt_less_nit ``` Andreas@47452 ` 1712` ``` tree_less_prop -> rbt_less_prop ``` Andreas@47452 ` 1713` ``` tree_less_simps -> rbt_less_simps ``` Andreas@47452 ` 1714` ``` tree_less_trans -> rbt_less_trans ``` Andreas@47452 ` 1715` ``` tree_ord_props -> rbt_ord_props ``` Andreas@47452 ` 1716` ``` union_Branch -> rbt_union_Branch ``` Andreas@47452 ` 1717` ``` union_is_rbt -> rbt_union_is_rbt ``` Andreas@47452 ` 1718` ``` unionw_is_rbt -> rbt_unionw_is_rbt ``` Andreas@47452 ` 1719` ``` unionwk_is_rbt -> rbt_unionwk_is_rbt ``` Andreas@47452 ` 1720` ``` unionwk_sorted -> rbt_unionwk_rbt_sorted ``` Andreas@47452 ` 1721` wenzelm@47807 ` 1722` ```* Theory HOL/Library/Float: Floating point numbers are now defined as ``` wenzelm@47807 ` 1723` ```a subset of the real numbers. All operations are defined using the ``` wenzelm@47807 ` 1724` ```lifing-framework and proofs use the transfer method. INCOMPATIBILITY. ``` hoelzl@47616 ` 1725` hoelzl@47616 ` 1726` ``` Changed Operations: ``` hoelzl@47622 ` 1727` ``` float_abs -> abs ``` hoelzl@47622 ` 1728` ``` float_nprt -> nprt ``` hoelzl@47622 ` 1729` ``` float_pprt -> pprt ``` hoelzl@47622 ` 1730` ``` pow2 -> use powr ``` hoelzl@47622 ` 1731` ``` round_down -> float_round_down ``` hoelzl@47622 ` 1732` ``` round_up -> float_round_up ``` hoelzl@47622 ` 1733` ``` scale -> exponent ``` hoelzl@47622 ` 1734` hoelzl@47622 ` 1735` ``` Removed Operations: ``` hoelzl@47622 ` 1736` ``` ceiling_fl, lb_mult, lb_mod, ub_mult, ub_mod ``` hoelzl@47622 ` 1737` hoelzl@47622 ` 1738` ``` Renamed Lemmas: ``` hoelzl@47622 ` 1739` ``` abs_float_def -> Float.compute_float_abs ``` hoelzl@47622 ` 1740` ``` bitlen_ge0 -> bitlen_nonneg ``` hoelzl@47622 ` 1741` ``` bitlen.simps -> Float.compute_bitlen ``` hoelzl@47622 ` 1742` ``` float_components -> Float_mantissa_exponent ``` hoelzl@47622 ` 1743` ``` float_divl.simps -> Float.compute_float_divl ``` hoelzl@47622 ` 1744` ``` float_divr.simps -> Float.compute_float_divr ``` hoelzl@47622 ` 1745` ``` float_eq_odd -> mult_powr_eq_mult_powr_iff ``` hoelzl@47622 ` 1746` ``` float_power -> real_of_float_power ``` hoelzl@47622 ` 1747` ``` lapprox_posrat_def -> Float.compute_lapprox_posrat ``` hoelzl@47622 ` 1748` ``` lapprox_rat.simps -> Float.compute_lapprox_rat ``` hoelzl@47622 ` 1749` ``` le_float_def' -> Float.compute_float_le ``` hoelzl@47622 ` 1750` ``` le_float_def -> less_eq_float.rep_eq ``` hoelzl@47622 ` 1751` ``` less_float_def' -> Float.compute_float_less ``` hoelzl@47622 ` 1752` ``` less_float_def -> less_float.rep_eq ``` hoelzl@47622 ` 1753` ``` normfloat_def -> Float.compute_normfloat ``` hoelzl@47622 ` 1754` ``` normfloat_imp_odd_or_zero -> mantissa_not_dvd and mantissa_noteq_0 ``` hoelzl@47622 ` 1755` ``` normfloat -> normfloat_def ``` hoelzl@47622 ` 1756` ``` normfloat_unique -> use normfloat_def ``` hoelzl@47622 ` 1757` ``` number_of_float_Float -> Float.compute_float_numeral, Float.compute_float_neg_numeral ``` hoelzl@47622 ` 1758` ``` one_float_def -> Float.compute_float_one ``` hoelzl@47622 ` 1759` ``` plus_float_def -> Float.compute_float_plus ``` hoelzl@47622 ` 1760` ``` rapprox_posrat_def -> Float.compute_rapprox_posrat ``` hoelzl@47622 ` 1761` ``` rapprox_rat.simps -> Float.compute_rapprox_rat ``` hoelzl@47622 ` 1762` ``` real_of_float_0 -> zero_float.rep_eq ``` hoelzl@47622 ` 1763` ``` real_of_float_1 -> one_float.rep_eq ``` hoelzl@47622 ` 1764` ``` real_of_float_abs -> abs_float.rep_eq ``` hoelzl@47622 ` 1765` ``` real_of_float_add -> plus_float.rep_eq ``` hoelzl@47622 ` 1766` ``` real_of_float_minus -> uminus_float.rep_eq ``` hoelzl@47622 ` 1767` ``` real_of_float_mult -> times_float.rep_eq ``` hoelzl@47622 ` 1768` ``` real_of_float_simp -> Float.rep_eq ``` hoelzl@47622 ` 1769` ``` real_of_float_sub -> minus_float.rep_eq ``` hoelzl@47622 ` 1770` ``` round_down.simps -> Float.compute_float_round_down ``` hoelzl@47622 ` 1771` ``` round_up.simps -> Float.compute_float_round_up ``` hoelzl@47622 ` 1772` ``` times_float_def -> Float.compute_float_times ``` hoelzl@47622 ` 1773` ``` uminus_float_def -> Float.compute_float_uminus ``` hoelzl@47622 ` 1774` ``` zero_float_def -> Float.compute_float_zero ``` hoelzl@47622 ` 1775` hoelzl@47622 ` 1776` ``` Lemmas not necessary anymore, use the transfer method: ``` hoelzl@47622 ` 1777` ``` bitlen_B0, bitlen_B1, bitlen_ge1, bitlen_Min, bitlen_Pls, float_divl, ``` hoelzl@47622 ` 1778` ``` float_divr, float_le_simp, float_less1_mantissa_bound, ``` hoelzl@47622 ` 1779` ``` float_less_simp, float_less_zero, float_le_zero, ``` hoelzl@47622 ` 1780` ``` float_pos_less1_e_neg, float_pos_m_pos, float_split, float_split2, ``` hoelzl@47622 ` 1781` ``` floor_pos_exp, lapprox_posrat, lapprox_posrat_bottom, lapprox_rat, ``` hoelzl@47622 ` 1782` ``` lapprox_rat_bottom, normalized_float, rapprox_posrat, ``` hoelzl@47622 ` 1783` ``` rapprox_posrat_le1, rapprox_rat, real_of_float_ge0_exp, ``` hoelzl@47622 ` 1784` ``` real_of_float_neg_exp, real_of_float_nge0_exp, round_down floor_fl, ``` hoelzl@47622 ` 1785` ``` round_up, zero_le_float, zero_less_float ``` hoelzl@47616 ` 1786` wenzelm@47856 ` 1787` ```* New theory HOL/Library/DAList provides an abstract type for ``` wenzelm@47856 ` 1788` ```association lists with distinct keys. ``` noschinl@45791 ` 1789` wenzelm@47866 ` 1790` ```* Session HOL/IMP: Added new theory of abstract interpretation of ``` wenzelm@47866 ` 1791` ```annotated commands. ``` wenzelm@47866 ` 1792` wenzelm@47855 ` 1793` ```* Session HOL-Import: Re-implementation from scratch is faster, ``` wenzelm@47855 ` 1794` ```simpler, and more scalable. Requires a proof bundle, which is ``` wenzelm@47855 ` 1795` ```available as an external component. Discontinued old (and mostly ``` wenzelm@47855 ` 1796` ```dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY. ``` wenzelm@47855 ` 1797` wenzelm@47855 ` 1798` ```* Session HOL-Word: Discontinued many redundant theorems specific to ``` wenzelm@47855 ` 1799` ```type 'a word. INCOMPATIBILITY, use the corresponding generic theorems ``` wenzelm@47855 ` 1800` ```instead. ``` wenzelm@47855 ` 1801` wenzelm@47855 ` 1802` ``` word_sub_alt ~> word_sub_wi ``` wenzelm@47855 ` 1803` ``` word_add_alt ~> word_add_def ``` wenzelm@47855 ` 1804` ``` word_mult_alt ~> word_mult_def ``` wenzelm@47855 ` 1805` ``` word_minus_alt ~> word_minus_def ``` wenzelm@47855 ` 1806` ``` word_0_alt ~> word_0_wi ``` wenzelm@47855 ` 1807` ``` word_1_alt ~> word_1_wi ``` wenzelm@47855 ` 1808` ``` word_add_0 ~> add_0_left ``` wenzelm@47855 ` 1809` ``` word_add_0_right ~> add_0_right ``` wenzelm@47855 ` 1810` ``` word_mult_1 ~> mult_1_left ``` wenzelm@47855 ` 1811` ``` word_mult_1_right ~> mult_1_right ``` wenzelm@47855 ` 1812` ``` word_add_commute ~> add_commute ``` wenzelm@47855 ` 1813` ``` word_add_assoc ~> add_assoc ``` wenzelm@47855 ` 1814` ``` word_add_left_commute ~> add_left_commute ``` wenzelm@47855 ` 1815` ``` word_mult_commute ~> mult_commute ``` wenzelm@47855 ` 1816` ``` word_mult_assoc ~> mult_assoc ``` wenzelm@47855 ` 1817` ``` word_mult_left_commute ~> mult_left_commute ``` wenzelm@47855 ` 1818` ``` word_left_distrib ~> left_distrib ``` wenzelm@47855 ` 1819` ``` word_right_distrib ~> right_distrib ``` wenzelm@47855 ` 1820` ``` word_left_minus ~> left_minus ``` wenzelm@47855 ` 1821` ``` word_diff_0_right ~> diff_0_right ``` wenzelm@47855 ` 1822` ``` word_diff_self ~> diff_self ``` wenzelm@47855 ` 1823` ``` word_sub_def ~> diff_minus ``` wenzelm@47855 ` 1824` ``` word_diff_minus ~> diff_minus ``` wenzelm@47855 ` 1825` ``` word_add_ac ~> add_ac ``` wenzelm@47855 ` 1826` ``` word_mult_ac ~> mult_ac ``` wenzelm@47855 ` 1827` ``` word_plus_ac0 ~> add_0_left add_0_right add_ac ``` wenzelm@47855 ` 1828` ``` word_times_ac1 ~> mult_1_left mult_1_right mult_ac ``` wenzelm@47855 ` 1829` ``` word_order_trans ~> order_trans ``` wenzelm@47855 ` 1830` ``` word_order_refl ~> order_refl ``` wenzelm@47855 ` 1831` ``` word_order_antisym ~> order_antisym ``` wenzelm@47855 ` 1832` ``` word_order_linear ~> linorder_linear ``` wenzelm@47855 ` 1833` ``` lenw1_zero_neq_one ~> zero_neq_one ``` wenzelm@47855 ` 1834` ``` word_number_of_eq ~> number_of_eq ``` wenzelm@47855 ` 1835` ``` word_of_int_add_hom ~> wi_hom_add ``` wenzelm@47855 ` 1836` ``` word_of_int_sub_hom ~> wi_hom_sub ``` wenzelm@47855 ` 1837` ``` word_of_int_mult_hom ~> wi_hom_mult ``` wenzelm@47855 ` 1838` ``` word_of_int_minus_hom ~> wi_hom_neg ``` wenzelm@47855 ` 1839` ``` word_of_int_succ_hom ~> wi_hom_succ ``` wenzelm@47855 ` 1840` ``` word_of_int_pred_hom ~> wi_hom_pred ``` wenzelm@47855 ` 1841` ``` word_of_int_0_hom ~> word_0_wi ``` wenzelm@47855 ` 1842` ``` word_of_int_1_hom ~> word_1_wi ``` wenzelm@47855 ` 1843` wenzelm@47809 ` 1844` ```* Session HOL-Word: New proof method "word_bitwise" for splitting ``` wenzelm@47809 ` 1845` ```machine word equalities and inequalities into logical circuits, ``` wenzelm@47809 ` 1846` ```defined in HOL/Word/WordBitwise.thy. Supports addition, subtraction, ``` wenzelm@47809 ` 1847` ```multiplication, shifting by constants, bitwise operators and numeric ``` wenzelm@47809 ` 1848` ```constants. Requires fixed-length word types, not 'a word. Solves ``` wenzelm@47854 ` 1849` ```many standard word identities outright and converts more into first ``` wenzelm@47809 ` 1850` ```order problems amenable to blast or similar. See also examples in ``` wenzelm@47809 ` 1851` ```HOL/Word/Examples/WordExamples.thy. ``` wenzelm@47809 ` 1852` wenzelm@47807 ` 1853` ```* Session HOL-Probability: Introduced the type "'a measure" to ``` wenzelm@47807 ` 1854` ```represent measures, this replaces the records 'a algebra and 'a ``` wenzelm@47807 ` 1855` ```measure_space. The locales based on subset_class now have two ``` wenzelm@47856 ` 1856` ```locale-parameters the space \ and the set of measurable sets M. ``` wenzelm@47856 ` 1857` ```The product of probability spaces uses now the same constant as the ``` wenzelm@47856 ` 1858` ```finite product of sigma-finite measure spaces "PiM :: ('i => 'a) ``` wenzelm@47807 ` 1859` ```measure". Most constants are defined now outside of locales and gain ``` wenzelm@47807 ` 1860` ```an additional parameter, like null_sets, almost_eventually or \'. ``` wenzelm@47807 ` 1861` ```Measure space constructions for distributions and densities now got ``` wenzelm@47807 ` 1862` ```their own constants distr and density. Instead of using locales to ``` wenzelm@47807 ` 1863` ```describe measure spaces with a finite space, the measure count_space ``` wenzelm@47807 ` 1864` ```and point_measure is introduced. INCOMPATIBILITY. ``` hoelzl@47694 ` 1865` hoelzl@47694 ` 1866` ``` Renamed constants: ``` hoelzl@47694 ` 1867` ``` measure -> emeasure ``` hoelzl@47694 ` 1868` ``` finite_measure.\' -> measure ``` hoelzl@47694 ` 1869` ``` product_algebra_generator -> prod_algebra ``` hoelzl@47694 ` 1870` ``` product_prob_space.emb -> prod_emb ``` hoelzl@47694 ` 1871` ``` product_prob_space.infprod_algebra -> PiM ``` hoelzl@47694 ` 1872` hoelzl@47694 ` 1873` ``` Removed locales: ``` hoelzl@47694 ` 1874` ``` completeable_measure_space ``` hoelzl@47694 ` 1875` ``` finite_measure_space ``` hoelzl@47694 ` 1876` ``` finite_prob_space ``` hoelzl@47694 ` 1877` ``` finite_product_finite_prob_space ``` hoelzl@47694 ` 1878` ``` finite_product_sigma_algebra ``` hoelzl@47694 ` 1879` ``` finite_sigma_algebra ``` hoelzl@47694 ` 1880` ``` measure_space ``` hoelzl@47694 ` 1881` ``` pair_finite_prob_space ``` hoelzl@47694 ` 1882` ``` pair_finite_sigma_algebra ``` hoelzl@47694 ` 1883` ``` pair_finite_space ``` hoelzl@47694 ` 1884` ``` pair_sigma_algebra ``` hoelzl@47694 ` 1885` ``` product_sigma_algebra ``` hoelzl@47694 ` 1886` hoelzl@47694 ` 1887` ``` Removed constants: ``` hoelzl@47751 ` 1888` ``` conditional_space ``` hoelzl@47694 ` 1889` ``` distribution -> use distr measure, or distributed predicate ``` hoelzl@47751 ` 1890` ``` image_space ``` hoelzl@47694 ` 1891` ``` joint_distribution -> use distr measure, or distributed predicate ``` hoelzl@47751 ` 1892` ``` pair_measure_generator ``` hoelzl@47694 ` 1893` ``` product_prob_space.infprod_algebra -> use PiM ``` hoelzl@47694 ` 1894` ``` subvimage ``` hoelzl@47694 ` 1895` hoelzl@47694 ` 1896` ``` Replacement theorems: ``` hoelzl@47751 ` 1897` ``` finite_additivity_sufficient -> ring_of_sets.countably_additiveI_finite ``` hoelzl@47751 ` 1898` ``` finite_measure.empty_measure -> measure_empty ``` hoelzl@47751 ` 1899` ``` finite_measure.finite_continuity_from_above -> finite_measure.finite_Lim_measure_decseq ``` hoelzl@47751 ` 1900` ``` finite_measure.finite_continuity_from_below -> finite_measure.finite_Lim_measure_incseq ``` hoelzl@47751 ` 1901` ``` finite_measure.finite_measure_countably_subadditive -> finite_measure.finite_measure_subadditive_countably ``` hoelzl@47751 ` 1902` ``` finite_measure.finite_measure_eq -> finite_measure.emeasure_eq_measure ``` hoelzl@47751 ` 1903` ``` finite_measure.finite_measure -> finite_measure.emeasure_finite ``` hoelzl@47751 ` 1904` ``` finite_measure.finite_measure_finite_singleton -> finite_measure.finite_measure_eq_setsum_singleton ``` hoelzl@47751 ` 1905` ``` finite_measure.positive_measure' -> measure_nonneg ``` hoelzl@47751 ` 1906` ``` finite_measure.real_measure -> finite_measure.emeasure_real ``` hoelzl@47751 ` 1907` ``` finite_product_prob_space.finite_measure_times -> finite_product_prob_space.finite_measure_PiM_emb ``` hoelzl@47751 ` 1908` ``` finite_product_sigma_algebra.in_P -> sets_PiM_I_finite ``` hoelzl@47751 ` 1909` ``` finite_product_sigma_algebra.P_empty -> space_PiM_empty, sets_PiM_empty ``` hoelzl@47751 ` 1910` ``` information_space.conditional_entropy_eq -> information_space.conditional_entropy_simple_distributed ``` hoelzl@47751 ` 1911` ``` information_space.conditional_entropy_positive -> information_space.conditional_entropy_nonneg_simple ``` hoelzl@47751 ` 1912` ``` information_space.conditional_mutual_information_eq_mutual_information -> information_space.conditional_mutual_information_eq_mutual_information_simple ``` hoelzl@47751 ` 1913` ``` information_space.conditional_mutual_information_generic_positive -> information_space.conditional_mutual_information_nonneg_simple ``` hoelzl@47751 ` 1914` ``` information_space.conditional_mutual_information_positive -> information_space.conditional_mutual_information_nonneg_simple ``` hoelzl@47751 ` 1915` ``` information_space.entropy_commute -> information_space.entropy_commute_simple ``` hoelzl@47751 ` 1916` ``` information_space.entropy_eq -> information_space.entropy_simple_distributed ``` hoelzl@47751 ` 1917` ``` information_space.entropy_generic_eq -> information_space.entropy_simple_distributed ``` hoelzl@47751 ` 1918` ``` information_space.entropy_positive -> information_space.entropy_nonneg_simple ``` hoelzl@47751 ` 1919` ``` information_space.entropy_uniform_max -> information_space.entropy_uniform ``` hoelzl@47751 ` 1920` ``` information_space.KL_eq_0_imp -> information_space.KL_eq_0_iff_eq ``` hoelzl@47751 ` 1921` ``` information_space.KL_eq_0 -> information_space.KL_same_eq_0 ``` hoelzl@47751 ` 1922` ``` information_space.KL_ge_0 -> information_space.KL_nonneg ``` hoelzl@47751 ` 1923` ``` information_space.mutual_information_eq -> information_space.mutual_information_simple_distributed ``` hoelzl@47751 ` 1924` ``` information_space.mutual_information_positive -> information_space.mutual_information_nonneg_simple ``` hoelzl@47751 ` 1925` ``` Int_stable_cuboids -> Int_stable_atLeastAtMost ``` hoelzl@47751 ` 1926` ``` Int_stable_product_algebra_generator -> positive_integral ``` hoelzl@47751 ` 1927` ``` measure_preserving -> equality "distr M N f = N" "f : measurable M N" ``` hoelzl@47694 ` 1928` ``` measure_space.additive -> emeasure_additive ``` hoelzl@47751 ` 1929` ``` measure_space.AE_iff_null_set -> AE_iff_null ``` hoelzl@47751 ` 1930` ``` measure_space.almost_everywhere_def -> eventually_ae_filter ``` hoelzl@47751 ` 1931` ``` measure_space.almost_everywhere_vimage -> AE_distrD ``` hoelzl@47751 ` 1932` ``` measure_space.continuity_from_above -> INF_emeasure_decseq ``` hoelzl@47751 ` 1933` ``` measure_space.continuity_from_above_Lim -> Lim_emeasure_decseq ``` hoelzl@47751 ` 1934` ``` measure_space.continuity_from_below_Lim -> Lim_emeasure_incseq ``` hoelzl@47694 ` 1935` ``` measure_space.continuity_from_below -> SUP_emeasure_incseq ``` hoelzl@47751 ` 1936` ``` measure_space_density -> emeasure_density ``` hoelzl@47751 ` 1937` ``` measure_space.density_is_absolutely_continuous -> absolutely_continuousI_density ``` hoelzl@47751 ` 1938` ``` measure_space.integrable_vimage -> integrable_distr ``` hoelzl@47751 ` 1939` ``` measure_space.integral_translated_density -> integral_density ``` hoelzl@47751 ` 1940` ``` measure_space.integral_vimage -> integral_distr ``` hoelzl@47751 ` 1941` ``` measure_space.measure_additive -> plus_emeasure ``` hoelzl@47751 ` 1942` ``` measure_space.measure_compl -> emeasure_compl ``` hoelzl@47751 ` 1943` ``` measure_space.measure_countable_increasing -> emeasure_countable_increasing ``` hoelzl@47751 ` 1944` ``` measure_space.measure_countably_subadditive -> emeasure_subadditive_countably ``` hoelzl@47694 ` 1945` ``` measure_space.measure_decseq -> decseq_emeasure ``` hoelzl@47751 ` 1946` ``` measure_space.measure_Diff -> emeasure_Diff ``` hoelzl@47751 ` 1947` ``` measure_space.measure_Diff_null_set -> emeasure_Diff_null_set ``` hoelzl@47694 ` 1948` ``` measure_space.measure_eq_0 -> emeasure_eq_0 ``` hoelzl@47694 ` 1949` ``` measure_space.measure_finitely_subadditive -> emeasure_subadditive_finite ``` hoelzl@47751 ` 1950` ``` measure_space.measure_finite_singleton -> emeasure_eq_setsum_singleton ``` hoelzl@47751 ` 1951` ``` measure_space.measure_incseq -> incseq_emeasure ``` hoelzl@47751 ` 1952` ``` measure_space.measure_insert -> emeasure_insert ``` hoelzl@47751 ` 1953` ``` measure_space.measure_mono -> emeasure_mono ``` hoelzl@47751 ` 1954` ``` measure_space.measure_not_negative -> emeasure_not_MInf ``` hoelzl@47751 ` 1955` ``` measure_space.measure_preserving_Int_stable -> measure_eqI_generator_eq ``` hoelzl@47751 ` 1956` ``` measure_space.measure_setsum -> setsum_emeasure ``` hoelzl@47751 ` 1957` ``` measure_space.measure_setsum_split -> setsum_emeasure_cover ``` hoelzl@47694 ` 1958` ``` measure_space.measure_space_vimage -> emeasure_distr ``` hoelzl@47751 ` 1959` ``` measure_space.measure_subadditive_finite -> emeasure_subadditive_finite ``` hoelzl@47751 ` 1960` ``` measure_space.measure_subadditive -> subadditive ``` hoelzl@47751 ` 1961` ``` measure_space.measure_top -> emeasure_space ``` hoelzl@47751 ` 1962` ``` measure_space.measure_UN_eq_0 -> emeasure_UN_eq_0 ``` hoelzl@47751 ` 1963` ``` measure_space.measure_Un_null_set -> emeasure_Un_null_set ``` hoelzl@47751 ` 1964` ``` measure_space.positive_integral_translated_density -> positive_integral_density ``` hoelzl@47751 ` 1965` ``` measure_space.positive_integral_vimage -> positive_integral_distr ``` hoelzl@47694 ` 1966` ``` measure_space.real_continuity_from_above -> Lim_measure_decseq ``` hoelzl@47751 ` 1967` ``` measure_space.real_continuity_from_below -> Lim_measure_incseq ``` hoelzl@47694 ` 1968` ``` measure_space.real_measure_countably_subadditive -> measure_subadditive_countably ``` hoelzl@47751 ` 1969` ``` measure_space.real_measure_Diff -> measure_Diff ``` hoelzl@47751 ` 1970` ``` measure_space.real_measure_finite_Union -> measure_finite_Union ``` hoelzl@47751 ` 1971` ``` measure_space.real_measure_setsum_singleton -> measure_eq_setsum_singleton ``` hoelzl@47751 ` 1972` ``` measure_space.real_measure_subadditive -> measure_subadditive ``` hoelzl@47751 ` 1973` ``` measure_space.real_measure_Union -> measure_Union ``` hoelzl@47751 ` 1974` ``` measure_space.real_measure_UNION -> measure_UNION ``` hoelzl@47694 ` 1975` ``` measure_space.simple_function_vimage -> simple_function_comp ``` hoelzl@47694 ` 1976` ``` measure_space.simple_integral_vimage -> simple_integral_distr ``` hoelzl@47751 ` 1977` ``` measure_space.simple_integral_vimage -> simple_integral_distr ``` hoelzl@47751 ` 1978` ``` measure_unique_Int_stable -> measure_eqI_generator_eq ``` hoelzl@47751 ` 1979` ``` measure_unique_Int_stable_vimage -> measure_eqI_generator_eq ``` hoelzl@47694 ` 1980` ``` pair_sigma_algebra.measurable_cut_fst -> sets_Pair1 ``` hoelzl@47694 ` 1981` ``` pair_sigma_algebra.measurable_cut_snd -> sets_Pair2 ``` hoelzl@47694 ` 1982` ``` pair_sigma_algebra.measurable_pair_image_fst -> measurable_Pair1 ``` hoelzl@47694 ` 1983` ``` pair_sigma_algebra.measurable_pair_image_snd -> measurable_Pair2 ``` hoelzl@47694 ` 1984` ``` pair_sigma_algebra.measurable_product_swap -> measurable_pair_swap_iff ``` hoelzl@47694 ` 1985` ``` pair_sigma_algebra.pair_sigma_algebra_measurable -> measurable_pair_swap ``` hoelzl@47694 ` 1986` ``` pair_sigma_algebra.pair_sigma_algebra_swap_measurable -> measurable_pair_swap' ``` hoelzl@47694 ` 1987` ``` pair_sigma_algebra.sets_swap -> sets_pair_swap ``` hoelzl@47751 ` 1988` ``` pair_sigma_finite.measure_cut_measurable_fst -> pair_sigma_finite.measurable_emeasure_Pair1 ``` hoelzl@47751 ` 1989` ``` pair_sigma_finite.measure_cut_measurable_snd -> pair_sigma_finite.measurable_emeasure_Pair2 ``` hoelzl@47751 ` 1990` ``` pair_sigma_finite.measure_preserving_swap -> pair_sigma_finite.distr_pair_swap ``` hoelzl@47751 ` 1991` ``` pair_sigma_finite.pair_measure_alt2 -> pair_sigma_finite.emeasure_pair_measure_alt2 ``` hoelzl@47751 ` 1992` ``` pair_sigma_finite.pair_measure_alt -> pair_sigma_finite.emeasure_pair_measure_alt ``` hoelzl@47751 ` 1993` ``` pair_sigma_finite.pair_measure_times -> pair_sigma_finite.emeasure_pair_measure_Times ``` hoelzl@47751 ` 1994` ``` prob_space.indep_distribution_eq_measure -> prob_space.indep_vars_iff_distr_eq_PiM ``` hoelzl@47751 ` 1995` ``` prob_space.indep_var_distributionD -> prob_space.indep_var_distribution_eq ``` hoelzl@47694 ` 1996` ``` prob_space.measure_space_1 -> prob_space.emeasure_space_1 ``` hoelzl@47694 ` 1997` ``` prob_space.prob_space_vimage -> prob_space_distr ``` hoelzl@47694 ` 1998` ``` prob_space.random_variable_restrict -> measurable_restrict ``` hoelzl@47751 ` 1999` ``` prob_space_unique_Int_stable -> measure_eqI_prob_space ``` hoelzl@47751 ` 2000` ``` product_algebraE -> prod_algebraE_all ``` hoelzl@47751 ` 2001` ``` product_algebra_generator_der -> prod_algebra_eq_finite ``` hoelzl@47751 ` 2002` ``` product_algebra_generator_into_space -> prod_algebra_sets_into_space ``` hoelzl@47751 ` 2003` ``` product_algebraI -> sets_PiM_I_finite ``` hoelzl@47751 ` 2004` ``` product_measure_exists -> product_sigma_finite.sigma_finite ``` hoelzl@47694 ` 2005` ``` product_prob_space.finite_index_eq_finite_product -> product_prob_space.sets_PiM_generator ``` hoelzl@47694 ` 2006` ``` product_prob_space.finite_measure_infprod_emb_Pi -> product_prob_space.measure_PiM_emb ``` hoelzl@47694 ` 2007` ``` product_prob_space.infprod_spec -> product_prob_space.emeasure_PiM_emb_not_empty ``` hoelzl@47694 ` 2008` ``` product_prob_space.measurable_component -> measurable_component_singleton ``` hoelzl@47694 ` 2009` ``` product_prob_space.measurable_emb -> measurable_prod_emb ``` hoelzl@47694 ` 2010` ``` product_prob_space.measurable_into_infprod_algebra -> measurable_PiM_single ``` hoelzl@47694 ` 2011` ``` product_prob_space.measurable_singleton_infprod -> measurable_component_singleton ``` hoelzl@47694 ` 2012` ``` product_prob_space.measure_emb -> emeasure_prod_emb ``` hoelzl@47751 ` 2013` ``` product_prob_space.measure_preserving_restrict -> product_prob_space.distr_restrict ``` hoelzl@47751 ` 2014` ``` product_sigma_algebra.product_algebra_into_space -> space_closed ``` hoelzl@47751 ` 2015` ``` product_sigma_finite.measure_fold -> product_sigma_finite.distr_merge ``` hoelzl@47751 ` 2016` ``` product_sigma_finite.measure_preserving_component_singelton -> product_sigma_finite.distr_singleton ``` hoelzl@47751 ` 2017` ``` product_sigma_finite.measure_preserving_merge -> product_sigma_finite.distr_merge ``` hoelzl@47694 ` 2018` ``` sequence_space.measure_infprod -> sequence_space.measure_PiM_countable ``` hoelzl@47751 ` 2019` ``` sets_product_algebra -> sets_PiM ``` hoelzl@47751 ` 2020` ``` sigma_algebra.measurable_sigma -> measurable_measure_of ``` hoelzl@47751 ` 2021` ``` sigma_finite_measure.disjoint_sigma_finite -> sigma_finite_disjoint ``` hoelzl@47751 ` 2022` ``` sigma_finite_measure.RN_deriv_vimage -> sigma_finite_measure.RN_deriv_distr ``` hoelzl@47751 ` 2023` ``` sigma_product_algebra_sigma_eq -> sigma_prod_algebra_sigma_eq ``` hoelzl@47751 ` 2024` ``` space_product_algebra -> space_PiM ``` hoelzl@47694 ` 2025` wenzelm@47855 ` 2026` ```* Session HOL-TPTP: support to parse and import TPTP problems (all ``` wenzelm@47855 ` 2027` ```languages) into Isabelle/HOL. ``` wenzelm@47413 ` 2028` blanchet@45398 ` 2029` noschinl@45160 ` 2030` ```*** FOL *** ``` noschinl@45160 ` 2031` wenzelm@45383 ` 2032` ```* New "case_product" attribute (see HOL). ``` noschinl@45160 ` 2033` wenzelm@45109 ` 2034` wenzelm@47463 ` 2035` ```*** ZF *** ``` wenzelm@47463 ` 2036` wenzelm@47463 ` 2037` ```* Greater support for structured proofs involving induction or case ``` wenzelm@47463 ` 2038` ```analysis. ``` wenzelm@47463 ` 2039` wenzelm@47463 ` 2040` ```* Much greater use of mathematical symbols. ``` wenzelm@47463 ` 2041` wenzelm@47463 ` 2042` ```* Removal of many ML theorem bindings. INCOMPATIBILITY. ``` wenzelm@47463 ` 2043` wenzelm@47463 ` 2044` wenzelm@45128 ` 2045` ```*** ML *** ``` wenzelm@45128 ` 2046` wenzelm@46948 ` 2047` ```* Antiquotation @{keyword "name"} produces a parser for outer syntax ``` wenzelm@46948 ` 2048` ```from a minor keyword introduced via theory header declaration. ``` wenzelm@46948 ` 2049` wenzelm@46961 ` 2050` ```* Antiquotation @{command_spec "name"} produces the ``` wenzelm@46961 ` 2051` ```Outer_Syntax.command_spec from a major keyword introduced via theory ``` wenzelm@46961 ` 2052` ```header declaration; it can be passed to Outer_Syntax.command etc. ``` wenzelm@46961 ` 2053` wenzelm@46916 ` 2054` ```* Local_Theory.define no longer hard-wires default theorem name ``` wenzelm@46992 ` 2055` ```"foo_def", but retains the binding as given. If that is Binding.empty ``` wenzelm@46992 ` 2056` ```/ Attrib.empty_binding, the result is not registered as user-level ``` wenzelm@46992 ` 2057` ```fact. The Local_Theory.define_internal variant allows to specify a ``` wenzelm@46992 ` 2058` ```non-empty name (used for the foundation in the background theory), ``` wenzelm@46992 ` 2059` ```while omitting the fact binding in the user-context. Potential ``` wenzelm@46992 ` 2060` ```INCOMPATIBILITY for derived definitional packages: need to specify ``` wenzelm@46992 ` 2061` ```naming policy for primitive definitions more explicitly. ``` wenzelm@46916 ` 2062` wenzelm@46497 ` 2063` ```* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in ``` wenzelm@46497 ` 2064` ```conformance with similar operations in structure Term and Logic. ``` wenzelm@46497 ` 2065` wenzelm@45592 ` 2066` ```* Antiquotation @{attributes [...]} embeds attribute source ``` wenzelm@45592 ` 2067` ```representation into the ML text, which is particularly useful with ``` wenzelm@45592 ` 2068` ```declarations like Local_Theory.note. ``` wenzelm@45592 ` 2069` wenzelm@45128 ` 2070` ```* Structure Proof_Context follows standard naming scheme. Old ``` wenzelm@45128 ` 2071` ```ProofContext has been discontinued. INCOMPATIBILITY. ``` wenzelm@45128 ` 2072` wenzelm@45293 ` 2073` ```* Refined Local_Theory.declaration {syntax, pervasive}, with subtle ``` wenzelm@45298 ` 2074` ```change of semantics: update is applied to auxiliary local theory ``` wenzelm@45293 ` 2075` ```context as well. ``` wenzelm@45293 ` 2076` wenzelm@45620 ` 2077` ```* Modernized some old-style infix operations: ``` wenzelm@45620 ` 2078` wenzelm@45620 ` 2079` ``` addeqcongs ~> Simplifier.add_eqcong ``` wenzelm@45620 ` 2080` ``` deleqcongs ~> Simplifier.del_eqcong ``` wenzelm@45620 ` 2081` ``` addcongs ~> Simplifier.add_cong ``` wenzelm@45620 ` 2082` ``` delcongs ~> Simplifier.del_cong ``` wenzelm@45625 ` 2083` ``` setmksimps ~> Simplifier.set_mksimps ``` wenzelm@45625 ` 2084` ``` setmkcong ~> Simplifier.set_mkcong ``` wenzelm@45625 ` 2085` ``` setmksym ~> Simplifier.set_mksym ``` wenzelm@45625 ` 2086` ``` setmkeqTrue ~> Simplifier.set_mkeqTrue ``` wenzelm@45625 ` 2087` ``` settermless ~> Simplifier.set_termless ``` wenzelm@45625 ` 2088` ``` setsubgoaler ~> Simplifier.set_subgoaler ``` wenzelm@45620 ` 2089` ``` addsplits ~> Splitter.add_split ``` wenzelm@45620 ` 2090` ``` delsplits ~> Splitter.del_split ``` wenzelm@45620 ` 2091` wenzelm@45128 ` 2092` wenzelm@47461 ` 2093` ```*** System *** ``` wenzelm@47461 ` 2094` wenzelm@47661 ` 2095` ```* USER_HOME settings variable points to cross-platform user home ``` wenzelm@47661 ` 2096` ```directory, which coincides with HOME on POSIX systems only. Likewise, ``` wenzelm@47661 ` 2097` ```the Isabelle path specification "~" now expands to \$USER_HOME, instead ``` wenzelm@47661 ` 2098` ```of former \$HOME. A different default for USER_HOME may be set ``` wenzelm@47661 ` 2099` ```explicitly in shell environment, before Isabelle settings are ``` wenzelm@47661 ` 2100` ```evaluated. Minor INCOMPATIBILITY: need to adapt Isabelle path where ``` wenzelm@47661 ` 2101` ```the generic user home was intended. ``` wenzelm@47661 ` 2102` wenzelm@47807 ` 2103` ```* ISABELLE_HOME_WINDOWS refers to ISABELLE_HOME in windows file name ``` wenzelm@47807 ` 2104` ```notation, which is useful for the jEdit file browser, for example. ``` wenzelm@47807 ` 2105` wenzelm@47464 ` 2106` ```* ISABELLE_JDK_HOME settings variable points to JDK with javac and jar ``` wenzelm@47464 ` 2107` ```(not just JRE). ``` wenzelm@47464 ` 2108` wenzelm@47461 ` 2109` wenzelm@45109 ` 2110` wenzelm@44801 ` 2111` ```New in Isabelle2011-1 (October 2011) ``` wenzelm@44801 ` 2112` ```------------------------------------ ``` wenzelm@41651 ` 2113` wenzelm@41703 ` 2114` ```*** General *** ``` wenzelm@41703 ` 2115` wenzelm@44760 ` 2116` ```* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as ``` wenzelm@44968 ` 2117` ```"isabelle jedit" or "ISABELLE_HOME/Isabelle" on the command line. ``` wenzelm@44760 ` 2118` wenzelm@44777 ` 2119` ``` - Management of multiple theory files directly from the editor ``` wenzelm@44760 ` 2120` ``` buffer store -- bypassing the file-system (no requirement to save ``` wenzelm@44760 ` 2121` ``` files for checking). ``` wenzelm@44760 ` 2122` wenzelm@44777 ` 2123` ``` - Markup of formal entities within the text buffer, with semantic ``` wenzelm@44760 ` 2124` ``` highlighting, tooltips and hyperlinks to jump to defining source ``` wenzelm@44760 ` 2125` ``` positions. ``` wenzelm@44760 ` 2126` wenzelm@44777 ` 2127` ``` - Improved text rendering, with sub/superscripts in the source ``` wenzelm@44777 ` 2128` ``` buffer (including support for copy/paste wrt. output panel, HTML ``` wenzelm@44777 ` 2129` ``` theory output and other non-Isabelle text boxes). ``` wenzelm@44777 ` 2130` wenzelm@44777 ` 2131` ``` - Refined scheduling of proof checking and printing of results, ``` wenzelm@44760 ` 2132` ``` based on interactive editor view. (Note: jEdit folding and ``` wenzelm@44760 ` 2133` ``` narrowing allows to restrict buffer perspectives explicitly.) ``` wenzelm@44760 ` 2134` wenzelm@44777 ` 2135` ``` - Reduced CPU performance requirements, usable on machines with few ``` wenzelm@44760 ` 2136` ``` cores. ``` wenzelm@44760 ` 2137` wenzelm@44777 ` 2138` ``` - Reduced memory requirements due to pruning of unused document ``` wenzelm@44760 ` 2139` ``` versions (garbage collection). ``` wenzelm@44760 ` 2140` wenzelm@44760 ` 2141` ```See also ~~/src/Tools/jEdit/README.html for further information, ``` wenzelm@44760 ` 2142` ```including some remaining limitations. ``` wenzelm@44760 ` 2143` wenzelm@44800 ` 2144` ```* Theory loader: source files are exclusively located via the master ``` wenzelm@44800 ` 2145` ```directory of each theory node (where the .thy file itself resides). ``` wenzelm@44800 ` 2146` ```The global load path (such as src/HOL/Library) has been discontinued. ``` wenzelm@44800 ` 2147` ```Note that the path element ~~ may be used to reference theories in the ``` wenzelm@44800 ` 2148` ```Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet". ``` wenzelm@44800 ` 2149` ```INCOMPATIBILITY. ``` wenzelm@44800 ` 2150` wenzelm@41955 ` 2151` ```* Theory loader: source files are identified by content via SHA1 ``` wenzelm@41955 ` 2152` ```digests. Discontinued former path/modtime identification and optional ``` wenzelm@41955 ` 2153` ```ISABELLE_FILE_IDENT plugin scripts. ``` wenzelm@41955 ` 2154` wenzelm@41703 ` 2155` ```* Parallelization of nested Isar proofs is subject to ``` wenzelm@41703 ` 2156` ```Goal.parallel_proofs_threshold (default 100). See also isabelle ``` wenzelm@41703 ` 2157` ```usedir option -Q. ``` wenzelm@41703 ` 2158` wenzelm@42669 ` 2159` ```* Name space: former unsynchronized references are now proper ``` wenzelm@42669 ` 2160` ```configuration options, with more conventional names: ``` wenzelm@42669 ` 2161` wenzelm@42669 ` 2162` ``` long_names ~> names_long ``` wenzelm@42669 ` 2163` ``` short_names ~> names_short ``` wenzelm@42669 ` 2164` ``` unique_names ~> names_unique ``` wenzelm@42669 ` 2165` wenzelm@42669 ` 2166` ```Minor INCOMPATIBILITY, need to declare options in context like this: ``` wenzelm@42669 ` 2167` wenzelm@42669 ` 2168` ``` declare [[names_unique = false]] ``` wenzelm@42358 ` 2169` wenzelm@42502 ` 2170` ```* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`. Note ``` wenzelm@42502 ` 2171` ```that the result needs to be unique, which means fact specifications ``` wenzelm@42502 ` 2172` ```may have to be refined after enriching a proof context. ``` wenzelm@42502 ` 2173` wenzelm@44800 ` 2174` ```* Attribute "case_names" has been refined: the assumptions in each case ``` wenzelm@44800 ` 2175` ```can be named now by following the case name with [name1 name2 ...]. ``` wenzelm@44800 ` 2176` wenzelm@44968 ` 2177` ```* Isabelle/Isar reference manual has been updated and extended: ``` wenzelm@44968 ` 2178` ``` - "Synopsis" provides a catalog of main Isar language concepts. ``` wenzelm@44968 ` 2179` ``` - Formal references in syntax diagrams, via @{rail} antiquotation. ``` wenzelm@44968 ` 2180` ``` - Updated material from classic "ref" manual, notably about ``` wenzelm@44968 ` 2181` ``` "Classical Reasoner". ``` wenzelm@42633 ` 2182` wenzelm@41703 ` 2183` blanchet@41727 ` 2184` ```*** HOL *** ``` blanchet@41727 ` 2185` wenzelm@44968 ` 2186` ```* Class bot and top require underlying partial order rather than ``` wenzelm@44800 ` 2187` ```preorder: uniqueness of bot and top is guaranteed. INCOMPATIBILITY. ``` haftmann@43815 ` 2188` haftmann@43940 ` 2189` ```* Class complete_lattice: generalized a couple of lemmas from sets; ``` wenzelm@44800 ` 2190` ```generalized theorems INF_cong and SUP_cong. New type classes for ``` wenzelm@44800 ` 2191` ```complete boolean algebras and complete linear orders. Lemmas ``` wenzelm@44800 ` 2192` ```Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in ``` wenzelm@44800 ` 2193` ```class complete_linorder. ``` wenzelm@44800 ` 2194` wenzelm@44800 ` 2195` ```Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, ``` wenzelm@44800 ` 2196` ```Sup_fun_def, Inf_apply, Sup_apply. ``` wenzelm@44800 ` 2197` wenzelm@45088 ` 2198` ```Removed redundant lemmas (the right hand side gives hints how to ``` wenzelm@45088 ` 2199` ```replace them for (metis ...), or (simp only: ...) proofs): ``` hoelzl@45041 ` 2200` hoelzl@45041 ` 2201` ``` Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right] ``` hoelzl@45041 ` 2202` ``` Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right] ``` hoelzl@45041 ` 2203` ``` Inf_binary ~> Inf_insert, Inf_empty, and inf_top_right ``` hoelzl@45041 ` 2204` ``` Sup_binary ~> Sup_insert, Sup_empty, and sup_bot_right ``` hoelzl@45041 ` 2205` ``` Int_eq_Inter ~> Inf_insert, Inf_empty, and inf_top_right ``` hoelzl@45041 ` 2206` ``` Un_eq_Union ~> Sup_insert, Sup_empty, and sup_bot_right ``` hoelzl@45041 ` 2207` ``` Inter_def ~> INF_def, image_def ``` hoelzl@45041 ` 2208` ``` Union_def ~> SUP_def, image_def ``` hoelzl@45041 ` 2209` ``` INT_eq ~> INF_def, and image_def ``` hoelzl@45041 ` 2210` ``` UN_eq ~> SUP_def, and image_def ``` hoelzl@45041 ` 2211` ``` INF_subset ~> INF_superset_mono [OF _ order_refl] ``` wenzelm@44800 ` 2212` wenzelm@44800 ` 2213` ```More consistent and comprehensive names: ``` wenzelm@44800 ` 2214` hoelzl@45041 ` 2215` ``` INTER_eq_Inter_image ~> INF_def ``` hoelzl@45041 ` 2216` ``` UNION_eq_Union_image ~> SUP_def ``` haftmann@43872 ` 2217` ``` INFI_def ~> INF_def ``` haftmann@43872 ` 2218` ``` SUPR_def ~> SUP_def ``` haftmann@44103 ` 2219` ``` INF_leI ~> INF_lower ``` haftmann@44103 ` 2220` ``` INF_leI2 ~> INF_lower2 ``` haftmann@44103 ` 2221` ``` le_INFI ~> INF_greatest ``` haftmann@44103 ` 2222` ``` le_SUPI ~> SUP_upper ``` haftmann@44103 ` 2223` ``` le_SUPI2 ~> SUP_upper2 ``` haftmann@44103 ` 2224` ``` SUP_leI ~> SUP_least ``` haftmann@43873 ` 2225` ``` INFI_bool_eq ~> INF_bool_eq ``` haftmann@43873 ` 2226` ``` SUPR_bool_eq ~> SUP_bool_eq ``` haftmann@43873 ` 2227` ``` INFI_apply ~> INF_apply ``` haftmann@43873 ` 2228` ``` SUPR_apply ~> SUP_apply ``` haftmann@44103 ` 2229` ``` INTER_def ~> INTER_eq ``` haftmann@44103 ` 2230` ``` UNION_def ~> UNION_eq ``` haftmann@44103 ` 2231` haftmann@43865 ` 2232` ```INCOMPATIBILITY. ``` haftmann@43865 ` 2233` wenzelm@44973 ` 2234` ```* Renamed theory Complete_Lattice to Complete_Lattices. ``` wenzelm@44973 ` 2235` ```INCOMPATIBILITY. ``` wenzelm@44973 ` 2236` wenzelm@44973 ` 2237` ```* Theory Complete_Lattices: lemmas Inf_eq_top_iff, INF_eq_top_iff, ``` wenzelm@44973 ` 2238` ```INF_image, Inf_insert, INF_top, Inf_top_conv, INF_top_conv, SUP_bot, ``` wenzelm@44973 ` 2239` ```Sup_bot_conv, SUP_bot_conv, Sup_eq_top_iff, SUP_eq_top_iff, SUP_image, ``` wenzelm@44973 ` 2240` ```Sup_insert are now declared as [simp]. INCOMPATIBILITY. ``` wenzelm@44973 ` 2241` wenzelm@44973 ` 2242` ```* Theory Lattice: lemmas compl_inf_bot, compl_le_comp_iff, ``` wenzelm@44973 ` 2243` ```compl_sup_top, inf_idem, inf_left_idem, inf_sup_absorb, sup_idem, ``` wenzelm@44973 ` 2244` ```sup_inf_absob, sup_left_idem are now declared as [simp]. Minor ``` wenzelm@44973 ` 2245` ```INCOMPATIBILITY. ``` wenzelm@44973 ` 2246` krauss@44845 ` 2247` ```* Added syntactic classes "inf" and "sup" for the respective ``` krauss@44845 ` 2248` ```constants. INCOMPATIBILITY: Changes in the argument order of the ``` krauss@44845 ` 2249` ```(mostly internal) locale predicates for some derived classes. ``` krauss@44845 ` 2250` wenzelm@44800 ` 2251` ```* Theorem collections ball_simps and bex_simps do not contain theorems ``` wenzelm@44800 ` 2252` ```referring to UNION any longer; these have been moved to collection ``` wenzelm@44800 ` 2253` ```UN_ball_bex_simps. INCOMPATIBILITY. ``` wenzelm@44800 ` 2254` wenzelm@44800 ` 2255` ```* Theory Archimedean_Field: floor now is defined as parameter of a ``` wenzelm@44800 ` 2256` ```separate type class floor_ceiling. ``` wenzelm@44800 ` 2257` wenzelm@44800 ` 2258` ```* Theory Finite_Set: more coherent development of fold_set locales: ``` haftmann@42874 ` 2259` haftmann@42874 ` 2260` ``` locale fun_left_comm ~> locale comp_fun_commute ``` haftmann@42874 ` 2261` ``` locale fun_left_comm_idem ~> locale comp_fun_idem ``` wenzelm@44800 ` 2262` wenzelm@44800 ` 2263` ```Both use point-free characterization; interpretation proofs may need ``` wenzelm@44800 ` 2264` ```adjustment. INCOMPATIBILITY. ``` haftmann@42874 ` 2265` wenzelm@44800 ` 2266` ```* Theory Limits: Type "'a net" has been renamed to "'a filter", in ``` huffman@44081 ` 2267` ```accordance with standard mathematical terminology. INCOMPATIBILITY. ``` huffman@44081 ` 2268` wenzelm@44800 ` 2269` ```* Theory Complex_Main: The locale interpretations for the ``` wenzelm@44800 ` 2270` ```bounded_linear and bounded_bilinear locales have been removed, in ``` wenzelm@44800 ` 2271` ```order to reduce the number of duplicate lemmas. Users must use the ``` wenzelm@44800 ` 2272` ```original names for distributivity theorems, potential INCOMPATIBILITY. ``` huffman@44282 ` 2273` huffman@44282 ` 2274` ``` divide.add ~> add_divide_distrib ``` huffman@44282 ` 2275` ``` divide.diff ~> diff_divide_distrib ``` huffman@44282 ` 2276` ``` divide.setsum ~> setsum_divide_distrib ``` huffman@44282 ` 2277` ``` mult.add_right ~> right_distrib ``` huffman@44282 ` 2278` ``` mult.diff_right ~> right_diff_distrib ``` huffman@44282 ` 2279` ``` mult_right.setsum ~> setsum_right_distrib ``` huffman@44282 ` 2280` ``` mult_left.diff ~> left_diff_distrib ``` huffman@44282 ` 2281` wenzelm@44800 ` 2282` ```* Theory Complex_Main: Several redundant theorems have been removed or ``` huffman@44568 ` 2283` ```replaced by more general versions. INCOMPATIBILITY. ``` huffman@44522 ` 2284` huffman@45051 ` 2285` ``` real_diff_def ~> minus_real_def ``` huffman@45051 ` 2286` ``` real_divide_def ~> divide_real_def ``` huffman@45051 ` 2287` ``` real_less_def ~> less_le ``` huffman@45051 ` 2288` ``` real_abs_def ~> abs_real_def ``` huffman@45051 ` 2289` ``` real_sgn_def ~> sgn_real_def ``` huffman@45051 ` 2290` ``` real_mult_commute ~> mult_commute ``` huffman@45051 ` 2291` ``` real_mult_assoc ~> mult_assoc ``` huffman@45051 ` 2292` ``` real_mult_1 ~> mult_1_left ``` huffman@45051 ` 2293` ``` real_add_mult_distrib ~> left_distrib ``` huffman@45051 ` 2294` ``` real_zero_not_eq_one ~> zero_neq_one ``` huffman@45051 ` 2295` ``` real_mult_inverse_left ~> left_inverse ``` huffman@45051 ` 2296` ``` INVERSE_ZERO ~> inverse_zero ``` huffman@45051 ` 2297` ``` real_le_refl ~> order_refl ``` huffman@45051 ` 2298` ``` real_le_antisym ~> order_antisym ``` huffman@45051 ` 2299` ``` real_le_trans ~> order_trans ``` huffman@45051 ` 2300` ``` real_le_linear ~> linear ``` huffman@45051 ` 2301` ``` real_le_eq_diff ~> le_iff_diff_le_0 ``` huffman@45051 ` 2302` ``` real_add_left_mono ~> add_left_mono ``` huffman@45051 ` 2303` ``` real_mult_order ~> mult_pos_pos ``` huffman@45051 ` 2304` ``` real_mult_less_mono2 ~> mult_strict_left_mono ``` huffman@44822 ` 2305` ``` real_of_int_real_of_nat ~> real_of_int_of_nat_eq ``` huffman@44522 ` 2306` ``` real_0_le_divide_iff ~> zero_le_divide_iff ``` huffman@44522 ` 2307` ``` realpow_two_disj ~> power2_eq_iff ``` huffman@44522 ` 2308` ``` real_squared_diff_one_factored ~> square_diff_one_factored ``` huffman@44522 ` 2309` ``` realpow_two_diff ~> square_diff_square_factored ``` huffman@44669 ` 2310` ``` reals_complete2 ~> complete_real ``` huffman@44749 ` 2311` ``` real_sum_squared_expand ~> power2_sum ``` huffman@44522 ` 2312` ``` exp_ln_eq ~> ln_unique ``` huffman@44711 ` 2313` ``` expi_add ~> exp_add ``` huffman@44711 ` 2314` ``` expi_zero ~> exp_zero ``` huffman@44522 ` 2315` ``` lemma_DERIV_subst ~> DERIV_cong ``` huffman@44568 ` 2316` ``` LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff ``` huffman@44568 ` 2317` ``` LIMSEQ_const ~> tendsto_const ``` huffman@44568 ` 2318` ``` LIMSEQ_norm ~> tendsto_norm ``` huffman@44568 ` 2319` ``` LIMSEQ_add ~> tendsto_add ``` huffman@44568 ` 2320` ``` LIMSEQ_minus ~> tendsto_minus ``` huffman@44568 ` 2321` ``` LIMSEQ_minus_cancel ~> tendsto_minus_cancel ``` huffman@44568 ` 2322` ``` LIMSEQ_diff ~> tendsto_diff ``` huffman@44568 ` 2323` ``` bounded_linear.LIMSEQ ~> bounded_linear.tendsto ``` huffman@44568 ` 2324` ``` bounded_bilinear.LIMSEQ ~> bounded_bilinear.tendsto ``` huffman@44568 ` 2325` ``` LIMSEQ_mult ~> tendsto_mult ``` huffman@44568 ` 2326` ``` LIMSEQ_inverse ~> tendsto_inverse ``` huffman@44568 ` 2327` ``` LIMSEQ_divide ~> tendsto_divide ``` huffman@44568 ` 2328` ``` LIMSEQ_pow ~> tendsto_power ``` huffman@44568 ` 2329` ``` LIMSEQ_setsum ~> tendsto_setsum ``` huffman@44568 ` 2330` ``` LIMSEQ_setprod ~> tendsto_setprod ``` huffman@44568 ` 2331` ``` LIMSEQ_norm_zero ~> tendsto_norm_zero_iff ``` huffman@44568 ` 2332` ``` LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff ``` huffman@44568 ` 2333` ``` LIMSEQ_imp_rabs ~> tendsto_rabs ``` huffman@44710 ` 2334` ``` LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] ``` huffman@44710 ` 2335` ``` LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] ``` huffman@44710 ` 2336` ``` LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] ``` huffman@44748 ` 2337` ``` LIMSEQ_Complex ~> tendsto_Complex ``` huffman@44568 ` 2338` ``` LIM_ident ~> tendsto_ident_at ``` huffman@44568 ` 2339` ``` LIM_const ~> tendsto_const ``` huffman@44568 ` 2340` ``` LIM_add ~> tendsto_add ``` huffman@44568 ` 2341` ``` LIM_add_zero ~> tendsto_add_zero ``` huffman@44568 ` 2342` ``` LIM_minus ~> tendsto_minus ``` huffman@44568 ` 2343` ``` LIM_diff ~> tendsto_diff ``` huffman@44568 ` 2344` ``` LIM_norm ~> tendsto_norm ``` huffman@44568 ` 2345` ``` LIM_norm_zero ~> tendsto_norm_zero ``` huffman@44568 ` 2346` ``` LIM_norm_zero_cancel ~> tendsto_norm_zero_cancel ``` huffman@44568 ` 2347` ``` LIM_norm_zero_iff ~> tendsto_norm_zero_iff ``` huffman@44568 ` 2348` ``` LIM_rabs ~> tendsto_rabs ``` huffman@44568 ` 2349` ``` LIM_rabs_zero ~> tendsto_rabs_zero ``` huffman@44568 ` 2350` ``` LIM_rabs_zero_cancel ~> tendsto_rabs_zero_cancel ``` huffman@44568 ` 2351` ``` LIM_rabs_zero_iff ~> tendsto_rabs_zero_iff ``` huffman@44568 ` 2352` ``` LIM_compose ~> tendsto_compose ``` huffman@44568 ` 2353` ``` LIM_mult ~> tendsto_mult ``` huffman@44568 ` 2354` ``` LIM_scaleR ~> tendsto_scaleR ``` huffman@44568 ` 2355` ``` LIM_of_real ~> tendsto_of_real ``` huffman@44568 ` 2356` ``` LIM_power ~> tendsto_power ``` huffman@44568 ` 2357` ``` LIM_inverse ~> tendsto_inverse ``` huffman@44568 ` 2358` ``` LIM_sgn ~> tendsto_sgn ``` huffman@44568 ` 2359` ``` isCont_LIM_compose ~> isCont_tendsto_compose ``` huffman@44568 ` 2360` ``` bounded_linear.LIM ~> bounded_linear.tendsto ``` huffman@44568 ` 2361` ``` bounded_linear.LIM_zero ~> bounded_linear.tendsto_zero ``` huffman@44568 ` 2362` ``` bounded_bilinear.LIM ~> bounded_bilinear.tendsto ``` huffman@44568 ` 2363` ``` bounded_bilinear.LIM_prod_zero ~> bounded_bilinear.tendsto_zero ``` huffman@44568 ` 2364` ``` bounded_bilinear.LIM_left_zero ~> bounded_bilinear.tendsto_left_zero ``` huffman@44568 ` 2365` ``` bounded_bilinear.LIM_right_zero ~> bounded_bilinear.tendsto_right_zero ``` huffman@44568 ` 2366` ``` LIM_inverse_fun ~> tendsto_inverse [OF tendsto_ident_at] ``` huffman@44522 ` 2367` wenzelm@44967 ` 2368` ```* Theory Complex_Main: The definition of infinite series was ``` wenzelm@44967 ` 2369` ```generalized. Now it is defined on the type class {topological_space, ``` wenzelm@44967 ` 2370` ```comm_monoid_add}. Hence it is useable also for extended real numbers. ``` wenzelm@42484 ` 2371` huffman@44908 ` 2372` ```* Theory Complex_Main: The complex exponential function "expi" is now ``` huffman@44908 ` 2373` ```a type-constrained abbreviation for "exp :: complex => complex"; thus ``` huffman@44908 ` 2374` ```several polymorphic lemmas about "exp" are now applicable to "expi". ``` huffman@44908 ` 2375` wenzelm@44968 ` 2376` ```* Code generation: ``` wenzelm@44968 ` 2377` wenzelm@44968 ` 2378` ``` - Theory Library/Code_Char_ord provides native ordering of ``` wenzelm@44968 ` 2379` ``` characters in the target language. ``` wenzelm@44968 ` 2380` wenzelm@44968 ` 2381` ``` - Commands code_module and code_library are legacy, use export_code ``` wenzelm@44968 ` 2382` ``` instead. ``` wenzelm@44968 ` 2383` wenzelm@44968 ` 2384` ``` - Method "evaluation" is legacy, use method "eval" instead. ``` wenzelm@44968 ` 2385` wenzelm@44968 ` 2386` ``` - Legacy evaluator "SML" is deactivated by default. May be ``` wenzelm@44968 ` 2387` ``` reactivated by the following theory command: ``` wenzelm@44968 ` 2388` wenzelm@44968 ` 2389` ``` setup {* Value.add_evaluator ("SML", Codegen.eval_term) *} ``` wenzelm@44968 ` 2390` wenzelm@44968 ` 2391` ```* Declare ext [intro] by default. Rare INCOMPATIBILITY. ``` wenzelm@44968 ` 2392` wenzelm@45088 ` 2393` ```* New proof method "induction" that gives induction hypotheses the ``` wenzelm@45088 ` 2394` ```name "IH", thus distinguishing them from further hypotheses that come ``` wenzelm@45088 ` 2395` ```from rule induction. The latter are still called "hyps". Method ``` wenzelm@45088 ` 2396` ```"induction" is a thin wrapper around "induct" and follows the same ``` wenzelm@45088 ` 2397` ```syntax. ``` wenzelm@45088 ` 2398` wenzelm@44968 ` 2399` ```* Method "fastsimp" has been renamed to "fastforce", but "fastsimp" is ``` wenzelm@44968 ` 2400` ```still available as a legacy feature for some time. ``` wenzelm@44968 ` 2401` wenzelm@44968 ` 2402` ```* Nitpick: ``` wenzelm@44968 ` 2403` ``` - Added "need" and "total_consts" options. ``` wenzelm@44968 ` 2404` ``` - Reintroduced "show_skolems" option by popular demand. ``` wenzelm@44968 ` 2405` ``` - Renamed attribute: nitpick_def ~> nitpick_unfold. ``` wenzelm@44968 ` 2406` ``` INCOMPATIBILITY. ``` wenzelm@44968 ` 2407` wenzelm@44968 ` 2408` ```* Sledgehammer: ``` wenzelm@44968 ` 2409` ``` - Use quasi-sound (and efficient) translations by default. ``` wenzelm@44968 ` 2410` ``` - Added support for the following provers: E-ToFoF, LEO-II, ``` wenzelm@44968 ` 2411` ``` Satallax, SNARK, Waldmeister, and Z3 with TPTP syntax. ``` wenzelm@44968 ` 2412` ``` - Automatically preplay and minimize proofs before showing them if ``` wenzelm@44968 ` 2413` ``` this can be done within reasonable time. ``` wenzelm@44968 ` 2414` ``` - sledgehammer available_provers ~> sledgehammer supported_provers. ``` wenzelm@44968 ` 2415` ``` INCOMPATIBILITY. ``` wenzelm@44968 ` 2416` ``` - Added "preplay_timeout", "slicing", "type_enc", "sound", ``` wenzelm@44968 ` 2417` ``` "max_mono_iters", and "max_new_mono_instances" options. ``` wenzelm@44968 ` 2418` ``` - Removed "explicit_apply" and "full_types" options as well as "Full ``` wenzelm@44968 ` 2419` ``` Types" Proof General menu item. INCOMPATIBILITY. ``` wenzelm@44968 ` 2420` wenzelm@44968 ` 2421` ```* Metis: ``` wenzelm@44968 ` 2422` ``` - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY. ``` wenzelm@44968 ` 2423` ``` - Obsoleted "metisFT" -- use "metis (full_types)" instead. ``` wenzelm@44968 ` 2424` ``` INCOMPATIBILITY. ``` wenzelm@44968 ` 2425` wenzelm@44968 ` 2426` ```* Command 'try': ``` wenzelm@44968 ` 2427` ``` - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and ``` wenzelm@44968 ` 2428` ``` "elim:" options. INCOMPATIBILITY. ``` wenzelm@44968 ` 2429` ``` - Introduced 'try' that not only runs 'try_methods' but also ``` wenzelm@44968 ` 2430` ``` 'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'. ``` wenzelm@44968 ` 2431` wenzelm@44968 ` 2432` ```* Quickcheck: ``` wenzelm@44968 ` 2433` ``` - Added "eval" option to evaluate terms for the found counterexample ``` wenzelm@44968 ` 2434` ``` (currently only supported by the default (exhaustive) tester). ``` wenzelm@44968 ` 2435` ``` - Added post-processing of terms to obtain readable counterexamples ``` wenzelm@44968 ` 2436` ``` (currently only supported by the default (exhaustive) tester). ``` wenzelm@44968 ` 2437` ``` - New counterexample generator quickcheck[narrowing] enables ``` wenzelm@44968 ` 2438` ``` narrowing-based testing. Requires the Glasgow Haskell compiler ``` wenzelm@44968 ` 2439` ``` with its installation location defined in the Isabelle settings ``` wenzelm@44968 ` 2440` ``` environment as ISABELLE_GHC. ``` wenzelm@44968 ` 2441` ``` - Removed quickcheck tester "SML" based on the SML code generator ``` wenzelm@44968 ` 2442` ``` (formly in HOL/Library). ``` wenzelm@44968 ` 2443` wenzelm@44968 ` 2444` ```* Function package: discontinued option "tailrec". INCOMPATIBILITY, ``` wenzelm@44968 ` 2445` ```use 'partial_function' instead. ``` wenzelm@44968 ` 2446` wenzelm@44968 ` 2447` ```* Theory Library/Extended_Reals replaces now the positive extended ``` wenzelm@44968 ` 2448` ```reals found in probability theory. This file is extended by ``` wenzelm@44968 ` 2449` ```Multivariate_Analysis/Extended_Real_Limits. ``` wenzelm@44968 ` 2450` wenzelm@44974 ` 2451` ```* Theory Library/Old_Recdef: old 'recdef' package has been moved here, ``` wenzelm@44974 ` 2452` ```from where it must be imported explicitly if it is really required. ``` wenzelm@44974 ` 2453` ```INCOMPATIBILITY. ``` wenzelm@44968 ` 2454` wenzelm@44968 ` 2455` ```* Theory Library/Wfrec: well-founded recursion combinator "wfrec" has ``` wenzelm@44968 ` 2456` ```been moved here. INCOMPATIBILITY. ``` wenzelm@44968 ` 2457` wenzelm@44968 ` 2458` ```* Theory Library/Saturated provides type of numbers with saturated ``` wenzelm@44968 ` 2459` ```arithmetic. ``` wenzelm@44968 ` 2460` wenzelm@44968 ` 2461` ```* Theory Library/Product_Lattice defines a pointwise ordering for the ``` wenzelm@44968 ` 2462` ```product type 'a * 'b, and provides instance proofs for various order ``` wenzelm@44968 ` 2463` ```and lattice type classes. ``` wenzelm@44968 ` 2464` wenzelm@44968 ` 2465` ```* Theory Library/Countable now provides the "countable_datatype" proof ``` wenzelm@44968 ` 2466` ```method for proving "countable" class instances for datatypes. ``` wenzelm@44968 ` 2467` wenzelm@44968 ` 2468` ```* Theory Library/Cset_Monad allows do notation for computable sets ``` wenzelm@44968 ` 2469` ```(cset) via the generic monad ad-hoc overloading facility. ``` wenzelm@44968 ` 2470` wenzelm@44968 ` 2471` ```* Library: Theories of common data structures are split into theories ``` wenzelm@44968 ` 2472` ```for implementation, an invariant-ensuring type, and connection to an ``` wenzelm@44968 ` 2473` ```abstract type. INCOMPATIBILITY. ``` wenzelm@44968 ` 2474` wenzelm@44968 ` 2475` ``` - RBT is split into RBT and RBT_Mapping. ``` wenzelm@44968 ` 2476` ``` - AssocList is split and renamed into AList and AList_Mapping. ``` wenzelm@44968 ` 2477` ``` - DList is split into DList_Impl, DList, and DList_Cset. ``` wenzelm@44968 ` 2478` ``` - Cset is split into Cset and List_Cset. ``` wenzelm@44968 ` 2479` wenzelm@44968 ` 2480` ```* Theory Library/Nat_Infinity has been renamed to ``` wenzelm@44968 ` 2481` ```Library/Extended_Nat, with name changes of the following types and ``` wenzelm@44968 ` 2482` ```constants: ``` wenzelm@44968 ` 2483` wenzelm@44968 ` 2484` ``` type inat ~> type enat ``` wenzelm@44968 ` 2485` ``` Fin ~> enat ``` wenzelm@44968 ` 2486` ``` Infty ~> infinity (overloaded) ``` wenzelm@44968 ` 2487` ``` iSuc ~> eSuc ``` wenzelm@44968 ` 2488` ``` the_Fin ~> the_enat ``` wenzelm@44968 ` 2489` wenzelm@44968 ` 2490` ```Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has ``` wenzelm@44968 ` 2491` ```been renamed accordingly. INCOMPATIBILITY. ``` wenzelm@44968 ` 2492` wenzelm@44968 ` 2493` ```* Session Multivariate_Analysis: The euclidean_space type class now ``` wenzelm@44968 ` 2494` ```fixes a constant "Basis :: 'a set" consisting of the standard ``` wenzelm@44968 ` 2495` ```orthonormal basis for the type. Users now have the option of ``` wenzelm@44968 ` 2496` ```quantifying over this set instead of using the "basis" function, e.g. ``` wenzelm@44968 ` 2497` ```"ALL x:Basis. P x" vs "ALL i vec_eq_iff ``` wenzelm@44968 ` 2508` ``` dist_nth_le_cart ~> dist_vec_nth_le ``` wenzelm@44968 ` 2509` ``` tendsto_vector ~> vec_tendstoI ``` wenzelm@44968 ` 2510` ``` Cauchy_vector ~> vec_CauchyI ``` wenzelm@44968 ` 2511` wenzelm@44968 ` 2512` ```* Session Multivariate_Analysis: Several duplicate theorems have been ``` wenzelm@44968 ` 2513` ```removed, and other theorems have been renamed or replaced with more ``` wenzelm@44968 ` 2514` ```general versions. INCOMPATIBILITY. ``` wenzelm@44968 ` 2515` wenzelm@44968 ` 2516` ``` finite_choice ~> finite_set_choice ``` wenzelm@44968 ` 2517` ``` eventually_conjI ~> eventually_conj ``` wenzelm@44968 ` 2518` ``` eventually_and ~> eventually_conj_iff ``` wenzelm@44968 ` 2519` ``` eventually_false ~> eventually_False ``` wenzelm@44968 ` 2520` ``` setsum_norm ~> norm_setsum ``` wenzelm@44968 ` 2521` ``` Lim_sequentially ~> LIMSEQ_def ``` wenzelm@44968 ` 2522` ``` Lim_ident_at ~> LIM_ident ``` wenzelm@44968 ` 2523` ``` Lim_const ~> tendsto_const ``` wenzelm@44968 ` 2524` ``` Lim_cmul ~> tendsto_scaleR [OF tendsto_const] ``` wenzelm@44968 ` 2525` ``` Lim_neg ~> tendsto_minus ``` wenzelm@44968 ` 2526` ``` Lim_add ~> tendsto_add ``` wenzelm@44968 ` 2527` ``` Lim_sub ~> tendsto_diff ``` wenzelm@44968 ` 2528` ``` Lim_mul ~> tendsto_scaleR ``` wenzelm@44968 ` 2529` ``` Lim_vmul ~> tendsto_scaleR [OF _ tendsto_const] ``` wenzelm@44968 ` 2530` ``` Lim_null_norm ~> tendsto_norm_zero_iff [symmetric] ``` wenzelm@44968 ` 2531` ``` Lim_linear ~> bounded_linear.tendsto ``` wenzelm@44968 ` 2532` ``` Lim_component ~> tendsto_euclidean_component ``` wenzelm@44968 ` 2533` ``` Lim_component_cart ~> tendsto_vec_nth ``` wenzelm@44968 ` 2534` ``` Lim_inner ~> tendsto_inner [OF tendsto_const] ``` wenzelm@44968 ` 2535` ``` dot_lsum ~> inner_setsum_left ``` wenzelm@44968 ` 2536` ``` dot_rsum ~> inner_setsum_right ``` wenzelm@44968 ` 2537` ``` continuous_cmul ~> continuous_scaleR [OF continuous_const] ``` wenzelm@44968 ` 2538` ``` continuous_neg ~> continuous_minus ``` wenzelm@44968 ` 2539` ``` continuous_sub ~> continuous_diff ``` wenzelm@44968 ` 2540` ``` continuous_vmul ~> continuous_scaleR [OF _ continuous_const] ``` wenzelm@44968 ` 2541` ``` continuous_mul ~> continuous_scaleR ``` wenzelm@44968 ` 2542` ``` continuous_inv ~> continuous_inverse ``` wenzelm@44968 ` 2543` ``` continuous_at_within_inv ~> continuous_at_within_inverse ``` wenzelm@44968 ` 2544` ``` continuous_at_inv ~> continuous_at_inverse ``` wenzelm@44968 ` 2545` ``` continuous_at_norm ~> continuous_norm [OF continuous_at_id] ``` wenzelm@44968 ` 2546` ``` continuous_at_infnorm ~> continuous_infnorm [OF continuous_at_id] ``` wenzelm@44968 ` 2547` ``` continuous_at_component ~> continuous_component [OF continuous_at_id] ``` wenzelm@44968 ` 2548` ``` continuous_on_neg ~> continuous_on_minus ``` wenzelm@44968 ` 2549` ``` continuous_on_sub ~> continuous_on_diff ``` wenzelm@44968 ` 2550` ``` continuous_on_cmul ~> continuous_on_scaleR [OF continuous_on_const] ``` wenzelm@44968 ` 2551` ``` continuous_on_vmul ~> continuous_on_scaleR [OF _ continuous_on_const] ``` wenzelm@44968 ` 2552` ``` continuous_on_mul ~> continuous_on_scaleR ``` wenzelm@44968 ` 2553` ``` continuous_on_mul_real ~> continuous_on_mult ``` wenzelm@44968 ` 2554` ``` continuous_on_inner ~> continuous_on_inner [OF continuous_on_const] ``` wenzelm@44968 ` 2555` ``` continuous_on_norm ~> continuous_on_norm [OF continuous_on_id] ``` wenzelm@44968 ` 2556` ``` continuous_on_inverse ~> continuous_on_inv ``` wenzelm@44968 ` 2557` ``` uniformly_continuous_on_neg ~> uniformly_continuous_on_minus ``` wenzelm@44968 ` 2558` ``` uniformly_continuous_on_sub ~> uniformly_continuous_on_diff ``` wenzelm@44968 ` 2559` ``` subset_interior ~> interior_mono ``` wenzelm@44968 ` 2560` ``` subset_closure ~> closure_mono ``` wenzelm@44968 ` 2561` ``` closure_univ ~> closure_UNIV ``` wenzelm@44968 ` 2562` ``` real_arch_lt ~> reals_Archimedean2 ``` wenzelm@44968 ` 2563` ``` real_arch ~> reals_Archimedean3 ``` wenzelm@44968 ` 2564` ``` real_abs_norm ~> abs_norm_cancel ``` wenzelm@44968 ` 2565` ``` real_abs_sub_norm ~> norm_triangle_ineq3 ``` wenzelm@44968 ` 2566` ``` norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2 ``` wenzelm@44968 ` 2567` wenzelm@44968 ` 2568` ```* Session HOL-Probability: ``` wenzelm@44968 ` 2569` ``` - Caratheodory's extension lemma is now proved for ring_of_sets. ``` wenzelm@44968 ` 2570` ``` - Infinite products of probability measures are now available. ``` wenzelm@44968 ` 2571` ``` - Sigma closure is independent, if the generator is independent ``` wenzelm@44968 ` 2572` ``` - Use extended reals instead of positive extended ``` wenzelm@44968 ` 2573` ``` reals. INCOMPATIBILITY. ``` wenzelm@44968 ` 2574` huffman@45049 ` 2575` ```* Session HOLCF: Discontinued legacy theorem names, INCOMPATIBILITY. ``` huffman@45049 ` 2576` huffman@45049 ` 2577` ``` expand_fun_below ~> fun_below_iff ``` huffman@45049 ` 2578` ``` below_fun_ext ~> fun_belowI ``` huffman@45049 ` 2579` ``` expand_cfun_eq ~> cfun_eq_iff ``` huffman@45049 ` 2580` ``` ext_cfun ~> cfun_eqI ``` huffman@45049 ` 2581` ``` expand_cfun_below ~> cfun_below_iff ``` huffman@45049 ` 2582` ``` below_cfun_ext ~> cfun_belowI ``` huffman@45049 ` 2583` ``` monofun_fun_fun ~> fun_belowD ``` huffman@45049 ` 2584` ``` monofun_fun_arg ~> monofunE ``` huffman@45049 ` 2585` ``` monofun_lub_fun ~> adm_monofun [THEN admD] ``` huffman@45049 ` 2586` ``` cont_lub_fun ~> adm_cont [THEN admD] ``` huffman@45049 ` 2587` ``` cont2cont_Rep_CFun ~> cont2cont_APP ``` huffman@45049 ` 2588` ``` cont_Rep_CFun_app ~> cont_APP_app ``` huffman@45049 ` 2589` ``` cont_Rep_CFun_app_app ~> cont_APP_app_app ``` huffman@45049 ` 2590` ``` cont_cfun_fun ~> cont_Rep_cfun1 [THEN contE] ``` huffman@45049 ` 2591` ``` cont_cfun_arg ~> cont_Rep_cfun2 [THEN contE] ``` huffman@45049 ` 2592` ``` contlub_cfun ~> lub_APP [symmetric] ``` huffman@45049 ` 2593` ``` contlub_LAM ~> lub_LAM [symmetric] ``` huffman@45049 ` 2594` ``` thelubI ~> lub_eqI ``` huffman@45049 ` 2595` ``` UU_I ~> bottomI ``` huffman@45049 ` 2596` ``` lift_distinct1 ~> lift.distinct(1) ``` huffman@45049 ` 2597` ``` lift_distinct2 ~> lift.distinct(2) ``` huffman@45049 ` 2598` ``` Def_not_UU ~> lift.distinct(2) ``` huffman@45049 ` 2599` ``` Def_inject ~> lift.inject ``` huffman@45049 ` 2600` ``` below_UU_iff ~> below_bottom_iff ``` huffman@45049 ` 2601` ``` eq_UU_iff ~> eq_bottom_iff ``` huffman@45049 ` 2602` huffman@44903 ` 2603` krauss@41685 ` 2604` ```*** Document preparation *** ``` krauss@41685 ` 2605` wenzelm@44800 ` 2606` ```* Antiquotation @{rail} layouts railroad syntax diagrams, see also ``` wenzelm@44800 ` 2607` ```isar-ref manual, both for description and actual application of the ``` wenzelm@44800 ` 2608` ```same. ``` wenzelm@44800 ` 2609` wenzelm@44800 ` 2610` ```* Antiquotation @{value} evaluates the given term and presents its ``` wenzelm@44800 ` 2611` ```result. ``` wenzelm@44800 ` 2612` wenzelm@44800 ` 2613` ```* Antiquotations: term style "isub" provides ad-hoc conversion of ``` wenzelm@44800 ` 2614` ```variables x1, y23 into subscripted form x\<^isub>1, ``` wenzelm@44800 ` 2615` ```y\<^isub>2\<^isub>3. ``` wenzelm@41651 ` 2616` wenzelm@42484 ` 2617` ```* Predefined LaTeX macros for Isabelle symbols \ and \ ``` wenzelm@42484 ` 2618` ```(e.g. see ~~/src/HOL/Library/Monad_Syntax.thy). ``` wenzelm@42484 ` 2619` wenzelm@44967 ` 2620` ```* Localized \isabellestyle switch can be used within blocks or groups ``` wenzelm@44967 ` 2621` ```like this: ``` wenzelm@44967 ` 2622` wenzelm@44967 ` 2623` ``` \isabellestyle{it} %preferred default ``` wenzelm@44967 ` 2624` ``` {\isabellestylett @{text "typewriter stuff"}} ``` wenzelm@44967 ` 2625` wenzelm@44967 ` 2626` ```* Discontinued special treatment of hard tabulators. Implicit ``` wenzelm@44967 ` 2627` ```tab-width is now defined as 1. Potential INCOMPATIBILITY for visual ``` wenzelm@44967 ` 2628` ```layouts. ``` wenzelm@44800 ` 2629` wenzelm@41651 ` 2630` wenzelm@41944 ` 2631` ```*** ML *** ``` wenzelm@41944 ` 2632` wenzelm@43731 ` 2633` ```* The inner syntax of sort/type/term/prop supports inlined YXML ``` wenzelm@43731 ` 2634` ```representations within quoted string tokens. By encoding logical ``` wenzelm@43731 ` 2635` ```entities via Term_XML (in ML or Scala) concrete syntax can be ``` wenzelm@43731 ` 2636` ```bypassed, which is particularly useful for producing bits of text ``` wenzelm@43731 ` 2637` ```under external program control. ``` wenzelm@43731 ` 2638` wenzelm@43565 ` 2639` ```* Antiquotations for ML and document preparation are managed as theory ``` wenzelm@43565 ` 2640` ```data, which requires explicit setup. ``` wenzelm@43565 ` 2641` wenzelm@42897 ` 2642` ```* Isabelle_Process.is_active allows tools to check if the official ``` wenzelm@42897 ` 2643` ```process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop ``` wenzelm@42897 ` 2644` ```(better known as Proof General). ``` wenzelm@42897 ` 2645` wenzelm@42360 ` 2646` ```* Structure Proof_Context follows standard naming scheme. Old ``` wenzelm@42360 ` 2647` ```ProofContext is still available for some time as legacy alias. ``` wenzelm@42360 ` 2648` wenzelm@42015 ` 2649` ```* Structure Timing provides various operations for timing; supersedes ``` wenzelm@42015 ` 2650` ```former start_timing/end_timing etc. ``` wenzelm@42015 ` 2651` wenzelm@41944 ` 2652` ```* Path.print is the official way to show file-system paths to users ``` wenzelm@41944 ` 2653` ```(including quotes etc.). ``` wenzelm@41944 ` 2654` wenzelm@42056 ` 2655` ```* Inner syntax: identifiers in parse trees of generic categories ``` wenzelm@42056 ` 2656` ```"logic", "aprop", "idt" etc. carry position information (disguised as ``` wenzelm@42056 ` 2657` ```type constraints). Occasional INCOMPATIBILITY with non-compliant ``` wenzelm@42057 ` 2658` ```translations that choke on unexpected type constraints. Positions can ``` wenzelm@42057 ` 2659` ```be stripped in ML translations via Syntax.strip_positions / ``` wenzelm@42057 ` 2660` ```Syntax.strip_positions_ast, or via the syntax constant ``` wenzelm@42057 ` 2661` ```"_strip_positions" within parse trees. As last resort, positions can ``` wenzelm@42057 ` 2662` ```be disabled via the configuration option Syntax.positions, which is ``` wenzelm@42057 ` 2663` ```called "syntax_positions" in Isar attribute syntax. ``` wenzelm@42056 ` 2664` wenzelm@42290 ` 2665` ```* Discontinued special status of various ML structures that contribute ``` wenzelm@42290 ` 2666` ```to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less ``` wenzelm@42290 ` 2667` ```pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY, ``` wenzelm@42290 ` 2668` ```refer directly to Ast.Constant, Lexicon.is_identifier, ``` wenzelm@42290 ` 2669` ```Syntax_Trans.mk_binder_tr etc. ``` wenzelm@42224 ` 2670` wenzelm@42247 ` 2671` ```* Typed print translation: discontinued show_sorts argument, which is ``` wenzelm@42247 ` 2672` ```already available via context of "advanced" translation. ``` wenzelm@42247 ` 2673` wenzelm@42370 ` 2674` ```* Refined PARALLEL_GOALS tactical: degrades gracefully for schematic ``` wenzelm@42370 ` 2675` ```goal states; body tactic needs to address all subgoals uniformly. ``` wenzelm@42370 ` 2676` wenzelm@42403 ` 2677` ```* Slightly more special eq_list/eq_set, with shortcut involving ``` wenzelm@42403 ` 2678` ```pointer equality (assumes that eq relation is reflexive). ``` wenzelm@42403 ` 2679` wenzelm@42793 ` 2680` ```* Classical tactics use proper Proof.context instead of historic types ``` wenzelm@42793 ` 2681` ```claset/clasimpset. Old-style declarations like addIs, addEs, addDs ``` wenzelm@42793 ` 2682` ```operate directly on Proof.context. Raw type claset retains its use as ``` wenzelm@42793 ` 2683` ```snapshot of the classical context, which can be recovered via ``` wenzelm@42793 ` 2684` ```(put_claset HOL_cs) etc. Type clasimpset has been discontinued. ``` wenzelm@42793 ` 2685` ```INCOMPATIBILITY, classical tactics and derived proof methods require ``` wenzelm@42793 ` 2686` ```proper Proof.context. ``` wenzelm@42793 ` 2687` wenzelm@44803 ` 2688` wenzelm@44803 ` 2689` ```*** System *** ``` wenzelm@44803 ` 2690` wenzelm@44968 ` 2691` ```* Discontinued support for Poly/ML 5.2, which was the last version ``` wenzelm@44968 ` 2692` ```without proper multithreading and TimeLimit implementation. ``` wenzelm@44968 ` 2693` wenzelm@44968 ` 2694` ```* Discontinued old lib/scripts/polyml-platform, which has been ``` wenzelm@44968 ` 2695` ```obsolete since Isabelle2009-2. ``` wenzelm@44968 ` 2696` wenzelm@44967 ` 2697` ```* Various optional external tools are referenced more robustly and ``` wenzelm@44967 ` 2698` ```uniformly by explicit Isabelle settings as follows: ``` wenzelm@44967 ` 2699` wenzelm@44967 ` 2700` ``` ISABELLE_CSDP (formerly CSDP_EXE) ``` wenzelm@44967 ` 2701` ``` ISABELLE_GHC (formerly EXEC_GHC or GHC_PATH) ``` wenzelm@44967 ` 2702` ``` ISABELLE_OCAML (formerly EXEC_OCAML) ``` wenzelm@44967 ` 2703` ``` ISABELLE_SWIPL (formerly EXEC_SWIPL) ``` wenzelm@44967 ` 2704` ``` ISABELLE_YAP (formerly EXEC_YAP) ``` wenzelm@44967 ` 2705` wenzelm@44967 ` 2706` ```Note that automated detection from the file-system or search path has ``` wenzelm@44967 ` 2707` ```been discontinued. INCOMPATIBILITY. ``` wenzelm@44967 ` 2708` wenzelm@43752 ` 2709` ```* Scala layer provides JVM method invocation service for static ``` wenzelm@44800 ` 2710` ```methods of type (String)String, see Invoke_Scala.method in ML. For ``` wenzelm@44800 ` 2711` ```example: ``` wenzelm@43752 ` 2712` wenzelm@43752 ` 2713` ``` Invoke_Scala.method "java.lang.System.getProperty" "java.home" ``` wenzelm@43752 ` 2714` wenzelm@44967 ` 2715` ```Together with YXML.string_of_body/parse_body and XML.Encode/Decode ``` wenzelm@44967 ` 2716` ```this allows to pass structured values between ML and Scala. ``` wenzelm@44800 ` 2717` wenzelm@44803 ` 2718` ```* The IsabelleText fonts includes some further glyphs to support the ``` wenzelm@44803 ` 2719` ```Prover IDE. Potential INCOMPATIBILITY: users who happen to have ``` wenzelm@44803 ` 2720` ```installed a local copy (which is normally *not* required) need to ``` wenzelm@44803 ` 2721` ```delete or update it from ~~/lib/fonts/. ``` wenzelm@41944 ` 2722` wenzelm@41703 ` 2723` wenzelm@45089 ` 2724` wenzelm@41512 ` 2725` ```New in Isabelle2011 (January 2011) ``` wenzelm@41512 ` 2726` ```---------------------------------- ``` wenzelm@37383 ` 2727` wenzelm@37536 ` 2728` ```*** General *** ``` wenzelm@37536 ` 2729` wenzelm@41573 ` 2730` ```* Experimental Prover IDE based on Isabelle/Scala and jEdit (see ``` wenzelm@41612 ` 2731` `src/Tools/jEdit). This also serves as IDE for Isabelle`