isabelle: NEWS@5f77017055a3 (annotated)

wenzelm@57491	1	Isabelle NEWS -- history of user-relevant changes
wenzelm@57491	2	=================================================
wenzelm@2553	3
wenzelm@62114	4	(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
wenzelm@60006	5
wenzelm@60331	6
wenzelm@62216	7	New in this Isabelle version
wenzelm@62216	8	----------------------------
wenzelm@62216	9
wenzelm@62440	10	* General *
wenzelm@62440	11
wenzelm@63120	12	* Embedded content (e.g. the inner syntax of types, terms, props) may be
wenzelm@63120	13	delimited uniformly via cartouches. This works better than old-fashioned
wenzelm@63120	14	quotes when sub-languages are nested.
wenzelm@63120	15
wenzelm@62958	16	* Type-inference improves sorts of newly introduced type variables for
wenzelm@62958	17	the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
wenzelm@62958	18	Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
wenzelm@62958	19	produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
wenzelm@62958	20	INCOMPATIBILITY, need to provide explicit type constraints for Pure
wenzelm@62958	21	types where this is really intended.
wenzelm@62958	22
wenzelm@62969	23	* Simplified outer syntax: uniform category "name" includes long
wenzelm@62969	24	identifiers. Former "xname" / "nameref" / "name reference" has been
wenzelm@62969	25	discontinued.
wenzelm@62969	26
wenzelm@62807	27	* Mixfix annotations support general block properties, with syntax
wenzelm@62807	28	"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
wenzelm@62807	29	"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
wenzelm@62807	30	to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
wenzelm@62807	31	is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
wenzelm@62789	32
wenzelm@62440	33	* New symbol \<circle>, e.g. for temporal operator.
wenzelm@62440	34
wenzelm@62453	35	* Old 'header' command is no longer supported (legacy since
wenzelm@62453	36	Isabelle2015).
wenzelm@62453	37
wenzelm@63273	38	* Command 'bundle' provides a local theory target to define a bundle
wenzelm@63273	39	from the body of specification commands (such as 'declare',
wenzelm@63273	40	'declaration', 'notation', 'lemmas', 'lemma'). For example:
wenzelm@63273	41
wenzelm@63273	42	bundle foo
wenzelm@63273	43	begin
wenzelm@63273	44	declare a [simp]
wenzelm@63273	45	declare b [intro]
wenzelm@63273	46	end
wenzelm@63272	47
wenzelm@63282	48	* Command 'unbundle' is like 'include', but works within a local theory
wenzelm@63282	49	context. Unlike "context includes ... begin", the effect of 'unbundle'
wenzelm@63282	50	on the target context persists, until different declarations are given.
wenzelm@63282	51
nipkow@63650	52	* Splitter in simp, auto and friends:
nipkow@63650	53	- The syntax "split add" has been discontinued, use plain "split".
nipkow@63656	54	- For situations with many conditional or case expressions,
nipkow@63650	55	there is an alternative splitting strategy that can be much faster.
nipkow@63650	56	It is selected by writing "split!" instead of "split". It applies
nipkow@63650	57	safe introduction and elimination rules after each split rule.
nipkow@63650	58	As a result the subgoal may be split into several subgoals.
nipkow@63650	59
wenzelm@63383	60	* Proof method "blast" is more robust wrt. corner cases of Pure
wenzelm@63383	61	statements without object-logic judgment.
wenzelm@63383	62
wenzelm@63532	63	* Pure provides basic versions of proof methods "simp" and "simp_all"
wenzelm@63532	64	that only know about meta-equality (==). Potential INCOMPATIBILITY in
wenzelm@63532	65	theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
wenzelm@63532	66	is relevant to avoid confusion of Pure.simp vs. HOL.simp.
wenzelm@63532	67
wenzelm@63624	68	* Commands 'prf' and 'full_prf' are somewhat more informative (again):
wenzelm@63624	69	proof terms are reconstructed and cleaned from administrative thm nodes.
wenzelm@63624	70
wenzelm@62440	71
wenzelm@62904	72	* Prover IDE -- Isabelle/Scala/jEdit *
wenzelm@62904	73
wenzelm@63135	74	* Cartouche abbreviations work both for " and ` to accomodate typical
wenzelm@63135	75	situations where old ASCII notation may be updated.
wenzelm@63135	76
wenzelm@63610	77	* Isabelle/ML and Standard ML files are presented in Sidekick with the
wenzelm@63610	78	tree structure of section headings: this special comment format is
wenzelm@63610	79	described in "implementation" chapter 0, e.g. (* section *).
wenzelm@63610	80
wenzelm@63022	81	* IDE support for the Isabelle/Pure bootstrap process, with the
wenzelm@63022	82	following independent stages:
wenzelm@63022	83
wenzelm@63022	84	src/Pure/ROOT0.ML
wenzelm@63022	85	src/Pure/ROOT.ML
wenzelm@63022	86	src/Pure/Pure.thy
wenzelm@63022	87	src/Pure/ML_Bootstrap.thy
wenzelm@63022	88
wenzelm@63022	89	The ML ROOT files act like quasi-theories in the context of theory
wenzelm@63022	90	ML_Bootstrap: this allows continuous checking of all loaded ML files.
wenzelm@63022	91	The theory files are presented with a modified header to import Pure
wenzelm@63022	92	from the running Isabelle instance. Results from changed versions of
wenzelm@63022	93	each stage are not propagated to the next stage, and isolated from the
wenzelm@63022	94	actual Isabelle/Pure that runs the IDE itself. The sequential
wenzelm@63307	95	dependencies of the above files are only observed for batch build.
wenzelm@62904	96
wenzelm@62987	97	* Highlighting of entity def/ref positions wrt. cursor.
wenzelm@62987	98
wenzelm@63461	99	* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
wenzelm@63592	100	are treated as delimiters for fold structure; 'begin' and 'end'
wenzelm@63592	101	structure of theory specifications is treated as well.
wenzelm@63461	102
wenzelm@63608	103	* Sidekick parser "isabelle-context" shows nesting of context blocks
wenzelm@63608	104	according to 'begin' and 'end' structure.
wenzelm@63608	105
wenzelm@63474	106	* Syntactic indentation according to Isabelle outer syntax. Action
wenzelm@63474	107	"indent-lines" (shortcut C+i) indents the current line according to
wenzelm@63474	108	command keywords and some command substructure. Action
wenzelm@63455	109	"isabelle.newline" (shortcut ENTER) indents the old and the new line
wenzelm@63455	110	according to command keywords only; see also option
wenzelm@63455	111	"jedit_indent_newline".
wenzelm@63452	112
wenzelm@63474	113	* Semantic indentation for unstructured proof scripts ('apply' etc.) via
wenzelm@63474	114	number of subgoals. This requires information of ongoing document
wenzelm@63474	115	processing and may thus lag behind, when the user is editing too
wenzelm@63474	116	quickly; see also option "jedit_script_indent" and
wenzelm@63474	117	"jedit_script_indent_limit".
wenzelm@63474	118
wenzelm@63236	119	* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
wenzelm@63236	120	occurences of the formal entity at the caret position. This facilitates
wenzelm@63236	121	systematic renaming.
wenzelm@63236	122
wenzelm@63751	123	* Action "isabelle.keymap-merge" asks the user to resolve pending
wenzelm@63751	124	Isabelle keymap changes that are in conflict with the current jEdit
wenzelm@63751	125	keymap; non-conflicting changes are always applied implicitly. This
wenzelm@63751	126	action is automatically invoked on Isabelle/jEdit startup and thus
wenzelm@63751	127	increases chances that users see new keyboard shortcuts when re-using
wenzelm@63751	128	old keymaps.
wenzelm@63751	129
wenzelm@63032	130	* Document markup works across multiple Isar commands, e.g. the results
wenzelm@63032	131	established at the end of a proof are properly identified in the theorem
wenzelm@63032	132	statement.
wenzelm@63032	133
wenzelm@63513	134	* Command 'proof' provides information about proof outline with cases,
wenzelm@63513	135	e.g. for proof methods "cases", "induct", "goal_cases".
wenzelm@63513	136
wenzelm@63528	137	* Completion templates for commands involving "begin ... end" blocks,
wenzelm@63528	138	e.g. 'context', 'notepad'.
wenzelm@63528	139
wenzelm@63581	140	* Additional abbreviations for syntactic completion may be specified
wenzelm@63579	141	within the theory header as 'abbrevs', in addition to global
wenzelm@63581	142	$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
wenzelm@63581	143	before. The theory syntax for 'keywords' has been simplified
wenzelm@63581	144	accordingly: optional abbrevs need to go into the new 'abbrevs' section.
wenzelm@63579	145
wenzelm@63675	146	* ML and document antiquotations for file-systems paths are more uniform
wenzelm@63675	147	and diverse:
wenzelm@63675	148
wenzelm@63675	149	@{path NAME} -- no file-system check
wenzelm@63675	150	@{file NAME} -- check for plain file
wenzelm@63675	151	@{dir NAME} -- check for directory
wenzelm@63675	152
wenzelm@63675	153	Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
wenzelm@63675	154	have to be changed.
wenzelm@63669	155
wenzelm@63669	156
wenzelm@62312	157	* Isar *
wenzelm@62312	158
wenzelm@63383	159	* The defining position of a literal fact \<open>prop\<close> is maintained more
wenzelm@63383	160	carefully, and made accessible as hyperlink in the Prover IDE.
wenzelm@63383	161
wenzelm@63383	162	* Commands 'finally' and 'ultimately' used to expose the result as
wenzelm@63383	163	literal fact: this accidental behaviour has been discontinued. Rare
wenzelm@63383	164	INCOMPATIBILITY, use more explicit means to refer to facts in Isar.
wenzelm@63383	165
wenzelm@63178	166	* Command 'axiomatization' has become more restrictive to correspond
wenzelm@63178	167	better to internal axioms as singleton facts with mandatory name. Minor
wenzelm@63178	168	INCOMPATIBILITY.
wenzelm@63178	169
wenzelm@63180	170	* Many specification elements support structured statements with 'if' /
wenzelm@63180	171	'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
wenzelm@63180	172	'definition', 'inductive', 'function'.
wenzelm@63180	173
wenzelm@63094	174	* Toplevel theorem statements support eigen-context notation with 'if' /
wenzelm@63284	175	'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
wenzelm@63094	176	traditional long statement form (in prefix). Local premises are called
wenzelm@63094	177	"that" or "assms", respectively. Empty premises are not bound in the
wenzelm@63094	178	context: INCOMPATIBILITY.
wenzelm@63094	179
wenzelm@63039	180	* Command 'define' introduces a local (non-polymorphic) definition, with
wenzelm@63039	181	optional abstraction over local parameters. The syntax resembles
wenzelm@63043	182	'definition' and 'obtain'. It fits better into the Isar language than
wenzelm@63043	183	old 'def', which is now a legacy feature.
wenzelm@63039	184
wenzelm@63059	185	* Command 'obtain' supports structured statements with 'if' / 'for'
wenzelm@63059	186	context.
wenzelm@63059	187
wenzelm@62312	188	* Command '\<proof>' is an alias for 'sorry', with different
wenzelm@62312	189	typesetting. E.g. to produce proof holes in examples and documentation.
wenzelm@62216	190
wenzelm@62939	191	* The old proof method "default" has been removed (legacy since
wenzelm@62939	192	Isabelle2016). INCOMPATIBILITY, use "standard" instead.
wenzelm@62939	193
wenzelm@63259	194	* Proof methods may refer to the main facts via the dynamic fact
wenzelm@63259	195	"method_facts". This is particularly useful for Eisbach method
wenzelm@63259	196	definitions.
wenzelm@63259	197
wenzelm@63527	198	* Proof method "use" allows to modify the main facts of a given method
wenzelm@63527	199	expression, e.g.
wenzelm@63259	200
wenzelm@63259	201	(use facts in simp)
wenzelm@63259	202	(use facts in \<open>simp add: ...\<close>)
wenzelm@63259	203
wenzelm@62216	204
haftmann@63165	205	* Pure *
haftmann@63165	206
wenzelm@63166	207	* Code generator: config option "code_timing" triggers measurements of
wenzelm@63166	208	different phases of code generation. See src/HOL/ex/Code_Timing.thy for
wenzelm@63166	209	examples.
haftmann@63165	210
haftmann@63350	211	* Code generator: implicits in Scala (stemming from type class instances)
haftmann@63350	212	are generated into companion object of corresponding type class, to resolve
haftmann@63350	213	some situations where ambiguities may occur.
haftmann@63350	214
haftmann@63165	215
blanchet@62327	216	* HOL *
blanchet@62327	217
hoelzl@63627	218	* Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
hoelzl@63627	219
hoelzl@63627	220	* Moved measure theory from HOL-Probability to HOL-Analysis. When importing
hoelzl@63627	221	HOL-Analysis some theorems need additional name spaces prefixes due to name
hoelzl@63627	222	clashes.
hoelzl@63627	223	INCOMPATIBILITY.
hoelzl@63627	224
eberlm@63635	225	* Number_Theory: algebraic foundation for primes: Generalisation of
eberlm@63635	226	predicate "prime" and introduction of predicates "prime_elem",
eberlm@63635	227	"irreducible", a "prime_factorization" function, and the "factorial_ring"
eberlm@63635	228	typeclass with instance proofs for nat, int, poly. Some theorems now have
eberlm@63635	229	different names, most notably "prime_def" is now "prime_nat_iff".
eberlm@63635	230	INCOMPATIBILITY.
eberlm@63552	231
eberlm@63552	232	* Probability: Code generation and QuickCheck for Probability Mass
eberlm@63552	233	Functions.
eberlm@63552	234
haftmann@63438	235	* Theory Set_Interval.thy: substantial new theorems on indexed sums
haftmann@63438	236	and products.
haftmann@63438	237
nipkow@63414	238	* Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying
nipkow@63414	239	equations in functional programming style: variables present on the
nipkow@63414	240	left-hand but not on the righ-hand side are replaced by underscores.
nipkow@63414	241
haftmann@63416	242	* "surj" is a mere input abbreviation, to avoid hiding an equation in
haftmann@63416	243	term output. Minor INCOMPATIBILITY.
haftmann@63416	244
haftmann@63377	245	* Theory Library/Combinator_PER.thy: combinator to build partial
haftmann@63378	246	equivalence relations from a predicate and an equivalence relation.
haftmann@63377	247
haftmann@63375	248	* Theory Library/Perm.thy: basic facts about almost everywhere fix
haftmann@63375	249	bijections.
haftmann@63375	250
haftmann@63374	251	* Locale bijection establishes convenient default simp rules
haftmann@63374	252	like "inv f (f a) = a" for total bijections.
haftmann@63374	253
wenzelm@63343	254	* Former locale lifting_syntax is now a bundle, which is easier to
wenzelm@63343	255	include in a local context or theorem statement, e.g. "context includes
wenzelm@63343	256	lifting_syntax begin ... end". Minor INCOMPATIBILITY.
wenzelm@63343	257
haftmann@63303	258	* Code generation for scala: ambiguous implicts in class diagrams
haftmann@63303	259	are spelt out explicitly.
haftmann@63303	260
haftmann@63290	261	* Abstract locales semigroup, abel_semigroup, semilattice,
haftmann@63290	262	semilattice_neutr, ordering, ordering_top, semilattice_order,
haftmann@63290	263	semilattice_neutr_order, comm_monoid_set, semilattice_set,
haftmann@63290	264	semilattice_neutr_set, semilattice_order_set, semilattice_order_neutr_set
haftmann@63290	265	monoid_list, comm_monoid_list, comm_monoid_list_set, comm_monoid_mset,
haftmann@63290	266	comm_monoid_fun use boldified syntax uniformly that does not clash
haftmann@63290	267	with corresponding global syntax. INCOMPATIBILITY.
haftmann@63290	268
haftmann@63237	269	* Conventional syntax "%(). t" for unit abstractions. Slight syntactic
haftmann@63237	270	INCOMPATIBILITY.
haftmann@63237	271
haftmann@63174	272	* Command 'code_reflect' accepts empty constructor lists for datatypes,
haftmann@63174	273	which renders those abstract effectively.
haftmann@63174	274
haftmann@63175	275	* Command 'export_code' checks given constants for abstraction violations:
haftmann@63175	276	a small guarantee that given constants specify a safe interface for the
haftmann@63175	277	generated code.
haftmann@63175	278
eberlm@63144	279	* Probability/Random_Permutations.thy contains some theory about
eberlm@63144	280	choosing a permutation of a set uniformly at random and folding over a
eberlm@63144	281	list in random order.
eberlm@63144	282
Andreas@63246	283	* Probability/SPMF formalises discrete subprobability distributions.
Andreas@63246	284
wenzelm@63283	285	* Library/FinFun.thy: bundles "finfun_syntax" and "no_finfun_syntax"
wenzelm@63283	286	allow to control optional syntax in local contexts; this supersedes
wenzelm@63283	287	former Library/FinFun_Syntax.thy. INCOMPATIBILITY, e.g. use "unbundle
wenzelm@63283	288	finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax".
wenzelm@63283	289
eberlm@63144	290	* Library/Set_Permutations.thy (executably) defines the set of
eberlm@63144	291	permutations of a set, i.e. the set of all lists that contain every
eberlm@63144	292	element of the carrier set exactly once.
eberlm@63144	293
haftmann@63161	294	* Static evaluators (Code_Evaluation.static_* in Isabelle/ML) rely on
haftmann@63161	295	explicitly provided auxiliary definitions for required type class
haftmann@63161	296	dictionaries rather than half-working magic. INCOMPATIBILITY, see
haftmann@63161	297	the tutorial on code generation for details.
haftmann@63161	298
wenzelm@62522	299	* New abbreviations for negated existence (but not bounded existence):
wenzelm@62522	300
wenzelm@62522	301	\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)
wenzelm@62522	302	\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)
wenzelm@62522	303
wenzelm@62521	304	* The print mode "HOL" for ASCII syntax of binders "!", "?", "?!", "@"
wenzelm@62521	305	has been removed for output. It is retained for input only, until it is
wenzelm@62521	306	eliminated altogether.
wenzelm@62521	307
blanchet@63785	308	* metis: The problem encoding has changed very slightly. This might
blanchet@63785	309	break existing proofs. INCOMPATIBILITY.
blanchet@63785	310
blanchet@63116	311	* Sledgehammer:
blanchet@63699	312	- The MaSh relevance filter has been sped up.
blanchet@63116	313	- Produce syntactically correct Vampire 4.0 problem files.
blanchet@63116	314
blanchet@62327	315	* (Co)datatype package:
blanchet@62693	316	- New commands for defining corecursive functions and reasoning about
blanchet@62693	317	them in "~~/src/HOL/Library/BNF_Corec.thy": 'corec', 'corecursive',
blanchet@62693	318	'friend_of_corec', and 'corecursion_upto'; and 'corec_unique' proof
blanchet@62842	319	method. See 'isabelle doc corec'.
blanchet@62693	320	- The predicator :: ('a => bool) => 'a F => bool is now a first-class
traytel@62332	321	citizen in bounded natural functors
blanchet@62693	322	- 'primrec' now allows nested calls through the predicator in addition
blanchet@62327	323	to the map function.
blanchet@62693	324	- 'bnf' automatically discharges reflexive proof obligations
blanchet@62693	325	- 'bnf' outputs a slightly modified proof obligation expressing rel in
traytel@62332	326	terms of map and set
traytel@62332	327	(not giving a specification for rel makes this one reflexive)
blanchet@62693	328	- 'bnf' outputs a new proof obligation expressing pred in terms of set
traytel@62332	329	(not giving a specification for pred makes this one reflexive)
blanchet@62693	330	INCOMPATIBILITY: manual 'bnf' declarations may need adjustment
blanchet@62335	331	- Renamed lemmas:
blanchet@62335	332	rel_prod_apply ~> rel_prod_inject
blanchet@62335	333	pred_prod_apply ~> pred_prod_inject
blanchet@62335	334	INCOMPATIBILITY.
blanchet@62536	335	- The "size" plugin has been made compatible again with locales.
blanchet@62327	336
wenzelm@63807	337	* Some old / obsolete theorems have been renamed / removed, potential
wenzelm@63807	338	INCOMPATIBILITY.
wenzelm@63807	339
wenzelm@63807	340	nat_less_cases -- removed, use linorder_cases instead
wenzelm@63807	341	inv_image_comp -- removed, use image_inv_f_f instead
wenzelm@63807	342	image_surj_f_inv_f ~> image_f_inv_f
wenzelm@63113	343
Mathias@63456	344	* Some theorems about groups and orders have been generalised from
Mathias@63456	345	groups to semi-groups that are also monoids:
Mathias@63456	346	le_add_same_cancel1
Mathias@63456	347	le_add_same_cancel2
Mathias@63456	348	less_add_same_cancel1
Mathias@63456	349	less_add_same_cancel2
Mathias@63456	350	add_le_same_cancel1
Mathias@63456	351	add_le_same_cancel2
Mathias@63456	352	add_less_same_cancel1
Mathias@63456	353	add_less_same_cancel2
Mathias@63456	354
Mathias@63456	355	* Some simplifications theorems about rings have been removed, since
Mathias@63456	356	superseeded by a more general version:
Mathias@63456	357	less_add_cancel_left_greater_zero ~> less_add_same_cancel1
Mathias@63456	358	less_add_cancel_right_greater_zero ~> less_add_same_cancel2
Mathias@63456	359	less_eq_add_cancel_left_greater_eq_zero ~> le_add_same_cancel1
Mathias@63456	360	less_eq_add_cancel_right_greater_eq_zero ~> le_add_same_cancel2
Mathias@63456	361	less_eq_add_cancel_left_less_eq_zero ~> add_le_same_cancel1
Mathias@63456	362	less_eq_add_cancel_right_less_eq_zero ~> add_le_same_cancel2
Mathias@63456	363	less_add_cancel_left_less_zero ~> add_less_same_cancel1
Mathias@63456	364	less_add_cancel_right_less_zero ~> add_less_same_cancel2
Mathias@63456	365	INCOMPATIBILITY.
Mathias@63456	366
wenzelm@62407	367	* Renamed split_if -> if_split and split_if_asm -> if_split_asm to
wenzelm@62407	368	resemble the f.split naming convention, INCOMPATIBILITY.
nipkow@62396	369
haftmann@62597	370	* Characters (type char) are modelled as finite algebraic type
haftmann@62597	371	corresponding to {0..255}.
haftmann@62597	372
haftmann@62597	373	- Logical representation:
haftmann@62597	374	* 0 is instantiated to the ASCII zero character.
wenzelm@62645	375	* All other characters are represented as "Char n"
haftmann@62597	376	with n being a raw numeral expression less than 256.
wenzelm@62645	377	* Expressions of the form "Char n" with n greater than 255
haftmann@62597	378	are non-canonical.
haftmann@62597	379	- Printing and parsing:
wenzelm@62645	380	* Printable characters are printed and parsed as "CHR ''\<dots>''"
haftmann@62597	381	(as before).
wenzelm@62645	382	* The ASCII zero character is printed and parsed as "0".
haftmann@62678	383	* All other canonical characters are printed as "CHR 0xXX"
haftmann@62678	384	with XX being the hexadecimal character code. "CHR n"
haftmann@62597	385	is parsable for every numeral expression n.
haftmann@62598	386	* Non-canonical characters have no special syntax and are
haftmann@62597	387	printed as their logical representation.
haftmann@62597	388	- Explicit conversions from and to the natural numbers are
haftmann@62597	389	provided as char_of_nat, nat_of_char (as before).
haftmann@62597	390	- The auxiliary nibble type has been discontinued.
haftmann@62597	391
haftmann@62597	392	INCOMPATIBILITY.
haftmann@62597	393
haftmann@62430	394	* Multiset membership is now expressed using set_mset rather than count.
haftmann@62430	395
haftmann@62430	396	- Expressions "count M a > 0" and similar simplify to membership
haftmann@62430	397	by default.
haftmann@62430	398
haftmann@62430	399	- Converting between "count M a = 0" and non-membership happens using
haftmann@62430	400	equations count_eq_zero_iff and not_in_iff.
haftmann@62430	401
haftmann@62430	402	- Rules count_inI and in_countE obtain facts of the form
haftmann@62430	403	"count M a = n" from membership.
haftmann@62430	404
haftmann@62430	405	- Rules count_in_diffI and in_diff_countE obtain facts of the form
haftmann@62430	406	"count M a = n + count N a" from membership on difference sets.
haftmann@62430	407
haftmann@62430	408	INCOMPATIBILITY.
haftmann@62430	409
Mathias@63310	410	* The names of multiset theorems have been normalised to distinguish which
Mathias@63310	411	ordering the theorems are about
Mathias@63310	412	mset_less_eqI ~> mset_subset_eqI
Mathias@63310	413	mset_less_insertD ~> mset_subset_insertD
Mathias@63310	414	mset_less_eq_count ~> mset_subset_eq_count
Mathias@63310	415	mset_less_diff_self ~> mset_subset_diff_self
Mathias@63310	416	mset_le_exists_conv ~> mset_subset_eq_exists_conv
Mathias@63310	417	mset_le_mono_add_right_cancel ~> mset_subset_eq_mono_add_right_cancel
Mathias@63310	418	mset_le_mono_add_left_cancel ~> mset_subset_eq_mono_add_left_cancel
Mathias@63310	419	mset_le_mono_add ~> mset_subset_eq_mono_add
Mathias@63310	420	mset_le_add_left ~> mset_subset_eq_add_left
Mathias@63310	421	mset_le_add_right ~> mset_subset_eq_add_right
Mathias@63310	422	mset_le_single ~> mset_subset_eq_single
Mathias@63310	423	mset_le_multiset_union_diff_commute ~> mset_subset_eq_multiset_union_diff_commute
Mathias@63310	424	diff_le_self ~> diff_subset_eq_self
Mathias@63310	425	mset_leD ~> mset_subset_eqD
Mathias@63310	426	mset_lessD ~> mset_subsetD
Mathias@63310	427	mset_le_insertD ~> mset_subset_eq_insertD
Mathias@63310	428	mset_less_of_empty ~> mset_subset_of_empty
Mathias@63310	429	le_empty ~> subset_eq_empty
Mathias@63310	430	mset_less_add_bothsides ~> mset_subset_add_bothsides
Mathias@63310	431	mset_less_empty_nonempty ~> mset_subset_empty_nonempty
Mathias@63310	432	mset_less_size ~> mset_subset_size
Mathias@63310	433	wf_less_mset_rel ~> wf_subset_mset_rel
Mathias@63310	434	count_le_replicate_mset_le ~> count_le_replicate_mset_subset_eq
Mathias@63310	435	mset_remdups_le ~> mset_remdups_subset_eq
Mathias@63310	436	ms_lesseq_impl ~> subset_eq_mset_impl
Mathias@63310	437
Mathias@63310	438	Some functions have been renamed:
Mathias@63310	439	ms_lesseq_impl -> subset_eq_mset_impl
Mathias@63310	440
Mathias@63388	441	* Multisets are now ordered with the multiset ordering
Mathias@63388	442	#\<subseteq># ~> \<le>
Mathias@63388	443	#\<subset># ~> <
Mathias@63388	444	le_multiset ~> less_eq_multiset
Mathias@63388	445	less_multiset ~> le_multiset
blanchet@63407	446	INCOMPATIBILITY.
Mathias@63388	447
Mathias@63388	448	* The prefix multiset_order has been discontinued: the theorems can be directly
blanchet@63407	449	accessed. As a consequence, the lemmas "order_multiset" and "linorder_multiset"
blanchet@63407	450	have been discontinued, and the interpretations "multiset_linorder" and
blanchet@63407	451	"multiset_wellorder" have been replaced by instantiations.
blanchet@63407	452	INCOMPATIBILITY.
Mathias@63388	453
Mathias@63388	454	* Some theorems about the multiset ordering have been renamed:
Mathias@63388	455	le_multiset_def ~> less_eq_multiset_def
Mathias@63388	456	less_multiset_def ~> le_multiset_def
Mathias@63388	457	less_eq_imp_le_multiset ~> subset_eq_imp_le_multiset
Mathias@63388	458	mult_less_not_refl ~> mset_le_not_refl
Mathias@63388	459	mult_less_trans ~> mset_le_trans
Mathias@63388	460	mult_less_not_sym ~> mset_le_not_sym
Mathias@63388	461	mult_less_asym ~> mset_le_asym
Mathias@63388	462	mult_less_irrefl ~> mset_le_irrefl
Mathias@63388	463	union_less_mono2{,1,2} ~> union_le_mono2{,1,2}
Mathias@63388	464
Mathias@63388	465	le_multiset\<^sub>H\<^sub>O ~> less_eq_multiset\<^sub>H\<^sub>O
Mathias@63388	466	le_multiset_total ~> less_eq_multiset_total
Mathias@63388	467	less_multiset_right_total ~> subset_eq_imp_le_multiset
Mathias@63388	468	le_multiset_empty_left ~> less_eq_multiset_empty_left
Mathias@63388	469	le_multiset_empty_right ~> less_eq_multiset_empty_right
Mathias@63388	470	less_multiset_empty_right ~> le_multiset_empty_left
Mathias@63388	471	less_multiset_empty_left ~> le_multiset_empty_right
Mathias@63388	472	union_less_diff_plus ~> union_le_diff_plus
Mathias@63388	473	ex_gt_count_imp_less_multiset ~> ex_gt_count_imp_le_multiset
Mathias@63388	474	less_multiset_plus_left_nonempty ~> le_multiset_plus_left_nonempty
Mathias@63388	475	le_multiset_plus_right_nonempty ~> le_multiset_plus_right_nonempty
Mathias@63388	476	less_multiset_plus_plus_left_iff ~> le_multiset_plus_plus_left_iff
Mathias@63388	477	less_multiset_plus_plus_right_iff ~> le_multiset_plus_plus_right_iff
blanchet@63407	478	INCOMPATIBILITY.
Mathias@63388	479
Mathias@63524	480	* The lemma mset_map has now the attribute [simp].
Mathias@63524	481	INCOMPATIBILITY.
Mathias@63524	482
Mathias@63525	483	* Some theorems about multisets have been removed:
Mathias@63525	484	le_multiset_plus_plus_left_iff ~> add_less_cancel_right
Mathias@63525	485	le_multiset_plus_plus_right_iff ~> add_less_cancel_left
Mathias@63525	486	add_eq_self_empty_iff ~> add_cancel_left_right
Mathias@63793	487	mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
Mathias@63525	488	INCOMPATIBILITY.
Mathias@63525	489
Mathias@63410	490	* Some typeclass constraints about multisets have been reduced from ordered or
Mathias@63410	491	linordered to preorder. Multisets have the additional typeclasses order_bot,
Mathias@63410	492	no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
Mathias@63525	493	linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.
Mathias@63410	494	INCOMPATIBILITY.
Mathias@63410	495
Mathias@63560	496	* There are some new simplification rules about multisets, the multiset
Mathias@63560	497	ordering, and the subset ordering on multisets.
Mathias@63560	498	INCOMPATIBILITY.
Mathias@63560	499
Mathias@63795	500	* The subset ordering on multisets has now the interpretations
Mathias@63795	501	ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot.
Mathias@63410	502	INCOMPATIBILITY.
Mathias@63410	503
Mathias@63793	504	* Multiset: single has been removed in favor of add_mset that roughly
Mathias@63793	505	corresponds to Set.insert. Some theorems have removed or changed:
Mathias@63793	506	single_not_empty ~> add_mset_not_empty or empty_not_add_mset
Mathias@63793	507	fold_mset_insert ~> fold_mset_add_mset
Mathias@63793	508	image_mset_insert ~> image_mset_add_mset
Mathias@63793	509	union_single_eq_diff
Mathias@63793	510	multi_self_add_other_not_self
Mathias@63793	511	diff_single_eq_union
Mathias@63793	512	INCOMPATIBILITY.
Mathias@63793	513
Mathias@63793	514	* Multiset: some theorems have been changed to use add_mset instead of single:
Mathias@63793	515	mset_add
Mathias@63793	516	multi_self_add_other_not_self
Mathias@63793	517	diff_single_eq_union
Mathias@63793	518	union_single_eq_diff
Mathias@63793	519	union_single_eq_member
Mathias@63793	520	add_eq_conv_diff
Mathias@63793	521	insert_noteq_member
Mathias@63793	522	add_eq_conv_ex
Mathias@63793	523	multi_member_split
Mathias@63793	524	multiset_add_sub_el_shuffle
Mathias@63793	525	mset_subset_eq_insertD
Mathias@63793	526	mset_subset_insertD
Mathias@63793	527	insert_subset_eq_iff
Mathias@63793	528	insert_union_subset_iff
Mathias@63793	529	multi_psub_of_add_self
Mathias@63793	530	inter_add_left1
Mathias@63793	531	inter_add_left2
Mathias@63793	532	inter_add_right1
Mathias@63793	533	inter_add_right2
Mathias@63793	534	sup_union_left1
Mathias@63793	535	sup_union_left2
Mathias@63793	536	sup_union_right1
Mathias@63793	537	sup_union_right2
Mathias@63793	538	size_eq_Suc_imp_eq_union
Mathias@63793	539	multi_nonempty_split
Mathias@63793	540	mset_insort
Mathias@63793	541	mset_update
Mathias@63793	542	mult1I
Mathias@63793	543	less_add
Mathias@63793	544	mset_zip_take_Cons_drop_twice
Mathias@63793	545	rel_mset_Zero
Mathias@63793	546	msed_map_invL
Mathias@63793	547	msed_map_invR
Mathias@63793	548	msed_rel_invL
Mathias@63793	549	msed_rel_invR
Mathias@63793	550	le_multiset_right_total
Mathias@63793	551	multiset_induct
Mathias@63793	552	multiset_induct2_size
Mathias@63793	553	multiset_induct2
Mathias@63793	554	INCOMPATIBILITY.
Mathias@63793	555
Mathias@63793	556	* Multiset: the definitions of some constants have changed to use add_mset instead
Mathias@63793	557	of adding a single element:
Mathias@63793	558	image_mset
Mathias@63793	559	mset
Mathias@63793	560	replicate_mset
Mathias@63793	561	mult1
Mathias@63793	562	pred_mset
Mathias@63793	563	rel_mset'
Mathias@63793	564	mset_insort
Mathias@63793	565	INCOMPATIBILITY.
Mathias@63793	566
Mathias@63793	567	* Due to the above changes, the attributes of some multiset theorems have
Mathias@63793	568	been changed:
Mathias@63793	569	insert_DiffM [] ~> [simp]
Mathias@63793	570	insert_DiffM2 [simp] ~> []
Mathias@63793	571	diff_add_mset_swap [simp]
Mathias@63793	572	fold_mset_add_mset [simp]
Mathias@63793	573	diff_diff_add [simp] (for multisets only)
Mathias@63793	574	diff_cancel [simp] ~> []
Mathias@63793	575	count_single [simp] ~> []
Mathias@63793	576	set_mset_single [simp] ~> []
Mathias@63793	577	size_multiset_single [simp] ~> []
Mathias@63793	578	size_single [simp] ~> []
Mathias@63793	579	image_mset_single [simp] ~> []
Mathias@63793	580	mset_subset_eq_mono_add_right_cancel [simp] ~> []
Mathias@63793	581	mset_subset_eq_mono_add_left_cancel [simp] ~> []
Mathias@63793	582	fold_mset_single [simp] ~> []
Mathias@63793	583	subset_eq_empty [simp] ~> []
Mathias@63795	584	empty_sup [simp] ~> []
Mathias@63795	585	sup_empty [simp] ~> []
Mathias@63795	586	inter_empty [simp] ~> []
Mathias@63795	587	empty_inter [simp] ~> []
Mathias@63793	588	INCOMPATIBILITY.
Mathias@63793	589
Mathias@63793	590	* The order of the variables in the second cases of multiset_induct,
Mathias@63793	591	multiset_induct2_size, multiset_induct2 has been changed (e.g. Add A a ~> Add a A).
Mathias@63793	592	INCOMPATIBILITY.
Mathias@63793	593
Mathias@63793	594	* There is now a simplification procedure on multisets. It mimics the behavior
Mathias@63793	595	of the procedure on natural numbers.
Mathias@63793	596	INCOMPATIBILITY.
Mathias@63793	597
Mathias@63795	598	* The lemma one_step_implies_mult_aux on multisets has been removed, use
Mathias@63795	599	one_step_implies_mult instead.
Mathias@63795	600	INCOMPATIBILITY.
Mathias@63795	601
haftmann@62343	602	* Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
haftmann@62343	603	INCOMPATIBILITY.
haftmann@62343	604
lp15@62408	605	* More complex analysis including Cauchy's inequality, Liouville theorem,
lp15@63078	606	open mapping theorem, maximum modulus principle, Residue theorem, Schwarz Lemma.
lp15@63078	607
lp15@63078	608	* Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
lp15@63078	609	Minkowski theorem.
lp15@62408	610
haftmann@62358	611	* "Gcd (f ` A)" and "Lcm (f ` A)" are printed with optional
haftmann@62358	612	comprehension-like syntax analogously to "Inf (f ` A)" and "Sup (f ` A)".
haftmann@62358	613
haftmann@62345	614	* Class semiring_Lcd merged into semiring_Gcd. INCOMPATIBILITY.
haftmann@62345	615
hoelzl@62376	616	* The type class ordered_comm_monoid_add is now called
hoelzl@62376	617	ordered_cancel_comm_monoid_add. A new type class ordered_comm_monoid_add is
hoelzl@62376	618	introduced as the combination of ordered_ab_semigroup_add + comm_monoid_add.
hoelzl@62376	619	INCOMPATIBILITY.
hoelzl@62376	620
hoelzl@62376	621	* Introduced the type classes canonically_ordered_comm_monoid_add and dioid.
hoelzl@62376	622
Mathias@63456	623	* Introduced the type class ordered_ab_semigroup_monoid_add_imp_le. When
Mathias@63456	624	instantiating linordered_semiring_strict and ordered_ab_group_add, an explicit
Mathias@63456	625	instantiation of ordered_ab_semigroup_monoid_add_imp_le might be
Mathias@63456	626	required.
Mathias@63456	627	INCOMPATIBILITY.
Mathias@63456	628
hoelzl@62376	629	* Added topological_monoid
hoelzl@62376	630
Andreas@62652	631	* Library/Complete_Partial_Order2.thy provides reasoning support for
Andreas@62652	632	proofs about monotonicity and continuity in chain-complete partial
Andreas@62652	633	orders and about admissibility conditions for fixpoint inductions.
Andreas@62652	634
haftmann@62352	635	* Library/Polynomial.thy contains also derivation of polynomials
haftmann@62352	636	but not gcd/lcm on polynomials over fields. This has been moved
haftmann@62352	637	to a separate theory Library/Polynomial_GCD_euclidean.thy, to
haftmann@62352	638	pave way for a possible future different type class instantiation
haftmann@62352	639	for polynomials over factorial rings. INCOMPATIBILITY.
haftmann@62352	640
nipkow@63155	641	* Library/Sublist.thy: added function "prefixes" and renamed
nipkow@63173	642	prefixeq -> prefix
nipkow@63173	643	prefix -> strict_prefix
nipkow@63173	644	suffixeq -> suffix
nipkow@63173	645	suffix -> strict_suffix
nipkow@63173	646	Added theory of longest common prefixes.
nipkow@63117	647
haftmann@62348	648	* Dropped various legacy fact bindings, whose replacements are often
haftmann@62348	649	of a more general type also:
haftmann@62348	650	lcm_left_commute_nat ~> lcm.left_commute
haftmann@62348	651	lcm_left_commute_int ~> lcm.left_commute
haftmann@62348	652	gcd_left_commute_nat ~> gcd.left_commute
haftmann@62348	653	gcd_left_commute_int ~> gcd.left_commute
haftmann@62348	654	gcd_greatest_iff_nat ~> gcd_greatest_iff
haftmann@62348	655	gcd_greatest_iff_int ~> gcd_greatest_iff
haftmann@62348	656	coprime_dvd_mult_nat ~> coprime_dvd_mult
haftmann@62348	657	coprime_dvd_mult_int ~> coprime_dvd_mult
haftmann@62348	658	zpower_numeral_even ~> power_numeral_even
haftmann@62348	659	gcd_mult_cancel_nat ~> gcd_mult_cancel
haftmann@62348	660	gcd_mult_cancel_int ~> gcd_mult_cancel
haftmann@62348	661	div_gcd_coprime_nat ~> div_gcd_coprime
haftmann@62348	662	div_gcd_coprime_int ~> div_gcd_coprime
haftmann@62348	663	zpower_numeral_odd ~> power_numeral_odd
haftmann@62348	664	zero_less_int_conv ~> of_nat_0_less_iff
haftmann@62348	665	gcd_greatest_nat ~> gcd_greatest
haftmann@62348	666	gcd_greatest_int ~> gcd_greatest
haftmann@62348	667	coprime_mult_nat ~> coprime_mult
haftmann@62348	668	coprime_mult_int ~> coprime_mult
haftmann@62348	669	lcm_commute_nat ~> lcm.commute
haftmann@62348	670	lcm_commute_int ~> lcm.commute
haftmann@62348	671	int_less_0_conv ~> of_nat_less_0_iff
haftmann@62348	672	gcd_commute_nat ~> gcd.commute
haftmann@62348	673	gcd_commute_int ~> gcd.commute
haftmann@62348	674	Gcd_insert_nat ~> Gcd_insert
haftmann@62348	675	Gcd_insert_int ~> Gcd_insert
haftmann@62348	676	of_int_int_eq ~> of_int_of_nat_eq
haftmann@62348	677	lcm_least_nat ~> lcm_least
haftmann@62348	678	lcm_least_int ~> lcm_least
haftmann@62348	679	lcm_assoc_nat ~> lcm.assoc
haftmann@62348	680	lcm_assoc_int ~> lcm.assoc
haftmann@62348	681	int_le_0_conv ~> of_nat_le_0_iff
haftmann@62348	682	int_eq_0_conv ~> of_nat_eq_0_iff
haftmann@62348	683	Gcd_empty_nat ~> Gcd_empty
haftmann@62348	684	Gcd_empty_int ~> Gcd_empty
haftmann@62348	685	gcd_assoc_nat ~> gcd.assoc
haftmann@62348	686	gcd_assoc_int ~> gcd.assoc
haftmann@62348	687	zero_zle_int ~> of_nat_0_le_iff
haftmann@62348	688	lcm_dvd2_nat ~> dvd_lcm2
haftmann@62348	689	lcm_dvd2_int ~> dvd_lcm2
haftmann@62348	690	lcm_dvd1_nat ~> dvd_lcm1
haftmann@62348	691	lcm_dvd1_int ~> dvd_lcm1
haftmann@62348	692	gcd_zero_nat ~> gcd_eq_0_iff
haftmann@62348	693	gcd_zero_int ~> gcd_eq_0_iff
haftmann@62348	694	gcd_dvd2_nat ~> gcd_dvd2
haftmann@62348	695	gcd_dvd2_int ~> gcd_dvd2
haftmann@62348	696	gcd_dvd1_nat ~> gcd_dvd1
haftmann@62348	697	gcd_dvd1_int ~> gcd_dvd1
haftmann@62348	698	int_numeral ~> of_nat_numeral
haftmann@62348	699	lcm_ac_nat ~> ac_simps
haftmann@62348	700	lcm_ac_int ~> ac_simps
haftmann@62348	701	gcd_ac_nat ~> ac_simps
haftmann@62348	702	gcd_ac_int ~> ac_simps
haftmann@62348	703	abs_int_eq ~> abs_of_nat
haftmann@62348	704	zless_int ~> of_nat_less_iff
haftmann@62348	705	zdiff_int ~> of_nat_diff
haftmann@62348	706	zadd_int ~> of_nat_add
haftmann@62348	707	int_mult ~> of_nat_mult
haftmann@62348	708	int_Suc ~> of_nat_Suc
haftmann@62348	709	inj_int ~> inj_of_nat
haftmann@62348	710	int_1 ~> of_nat_1
haftmann@62348	711	int_0 ~> of_nat_0
haftmann@62353	712	Lcm_empty_nat ~> Lcm_empty
haftmann@62353	713	Lcm_empty_int ~> Lcm_empty
haftmann@62353	714	Lcm_insert_nat ~> Lcm_insert
haftmann@62353	715	Lcm_insert_int ~> Lcm_insert
haftmann@62353	716	comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
haftmann@62353	717	comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
haftmann@62353	718	comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
haftmann@62353	719	comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
haftmann@62353	720	Lcm_eq_0 ~> Lcm_eq_0_I
haftmann@62353	721	Lcm0_iff ~> Lcm_0_iff
haftmann@62353	722	Lcm_dvd_int ~> Lcm_least
haftmann@62353	723	divides_mult_nat ~> divides_mult
haftmann@62353	724	divides_mult_int ~> divides_mult
haftmann@62353	725	lcm_0_nat ~> lcm_0_right
haftmann@62353	726	lcm_0_int ~> lcm_0_right
haftmann@62353	727	lcm_0_left_nat ~> lcm_0_left
haftmann@62353	728	lcm_0_left_int ~> lcm_0_left
haftmann@62353	729	dvd_gcd_D1_nat ~> dvd_gcdD1
haftmann@62353	730	dvd_gcd_D1_int ~> dvd_gcdD1
haftmann@62353	731	dvd_gcd_D2_nat ~> dvd_gcdD2
haftmann@62353	732	dvd_gcd_D2_int ~> dvd_gcdD2
haftmann@62353	733	coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
haftmann@62353	734	coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
haftmann@62348	735	realpow_minus_mult ~> power_minus_mult
haftmann@62348	736	realpow_Suc_le_self ~> power_Suc_le_self
haftmann@62353	737	dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
haftmann@62347	738	INCOMPATIBILITY.
haftmann@62347	739
wenzelm@62479	740	* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
wenzelm@62479	741
hoelzl@62975	742	* In HOL-Probability the type of emeasure and nn_integral was changed
hoelzl@62975	743	from ereal to ennreal:
hoelzl@62975	744	emeasure :: 'a measure => 'a set => ennreal
hoelzl@62975	745	nn_integral :: 'a measure => ('a => ennreal) => ennreal
hoelzl@62976	746	INCOMPATIBILITY.
blanchet@62327	747
wenzelm@63198	748
wenzelm@62498	749	* ML *
wenzelm@62498	750
wenzelm@63669	751	* ML antiquotation @{path} is superseded by @{file}, which ensures that
wenzelm@63669	752	the argument is a plain file. Minor INCOMPATIBILITY.
wenzelm@63669	753
wenzelm@63227	754	* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
wenzelm@63228	755	library (notably for big integers). Subtle change of semantics:
wenzelm@63228	756	Integer.gcd and Integer.lcm both normalize the sign, results are never
wenzelm@63228	757	negative. This coincides with the definitions in HOL/GCD.thy.
wenzelm@63228	758	INCOMPATIBILITY.
wenzelm@63227	759
wenzelm@63212	760	* Structure Rat for rational numbers is now an integral part of
wenzelm@63215	761	Isabelle/ML, with special notation @int/nat or @int for numerals (an
wenzelm@63215	762	abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
wenzelm@63212	763	printing. Standard operations on type Rat.rat are provided via ad-hoc
wenzelm@63215	764	overloading of + - * / < <= > >= ~ abs. INCOMPATIBILITY, need to
wenzelm@63212	765	use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been
wenzelm@63212	766	superseded by General.Div.
wenzelm@63198	767
wenzelm@62861	768	* The ML function "ML" provides easy access to run-time compilation.
wenzelm@62861	769	This is particularly useful for conditional compilation, without
wenzelm@62861	770	requiring separate files.
wenzelm@62861	771
wenzelm@62851	772	* Low-level ML system structures (like PolyML and RunCall) are no longer
wenzelm@62886	773	exposed to Isabelle/ML user-space. Potential INCOMPATIBILITY.
wenzelm@62851	774
wenzelm@62662	775	* Antiquotation @{make_string} is available during Pure bootstrap --
wenzelm@62662	776	with approximative output quality.
wenzelm@62662	777
wenzelm@62498	778	* Option ML_exception_debugger controls detailed exception trace via the
wenzelm@62498	779	Poly/ML debugger. Relevant ML modules need to be compiled beforehand
wenzelm@62498	780	with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
wenzelm@62498	781	debugger information requires consirable time and space: main
wenzelm@62498	782	Isabelle/HOL with full debugger support may need ML_system_64.
wenzelm@62498	783
wenzelm@62514	784	* Local_Theory.restore has been renamed to Local_Theory.reset to
wenzelm@62514	785	emphasize its disruptive impact on the cumulative context, notably the
wenzelm@62514	786	scope of 'private' or 'qualified' names. Note that Local_Theory.reset is
wenzelm@62514	787	only appropriate when targets are managed, e.g. starting from a global
wenzelm@62514	788	theory and returning to it. Regular definitional packages should use
wenzelm@62514	789	balanced blocks of Local_Theory.open_target versus
wenzelm@62514	790	Local_Theory.close_target instead. Rare INCOMPATIBILITY.
wenzelm@62514	791
wenzelm@62519	792	* Structure TimeLimit (originally from the SML/NJ library) has been
wenzelm@62519	793	replaced by structure Timeout, with slightly different signature.
wenzelm@62519	794	INCOMPATIBILITY.
wenzelm@62519	795
wenzelm@62551	796	* Discontinued cd and pwd operations, which are not well-defined in a
wenzelm@62551	797	multi-threaded environment. Note that files are usually located
wenzelm@62551	798	relatively to the master directory of a theory (see also
wenzelm@62551	799	File.full_path). Potential INCOMPATIBILITY.
wenzelm@62551	800
wenzelm@63352	801	* Binding.empty_atts supersedes Thm.empty_binding and
wenzelm@63352	802	Attrib.empty_binding. Minor INCOMPATIBILITY.
wenzelm@63352	803
wenzelm@62498	804
wenzelm@62354	805	* System *
wenzelm@62354	806
wenzelm@62840	807	* Many Isabelle tools that require a Java runtime system refer to the
wenzelm@62840	808	settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
wenzelm@62840	809	depending on the underlying platform. The settings for "isabelle build"
wenzelm@62840	810	ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
wenzelm@62840	811	discontinued. Potential INCOMPATIBILITY.
wenzelm@62840	812
wenzelm@62591	813	* The Isabelle system environment always ensures that the main
wenzelm@62591	814	executables are found within the shell search $PATH: "isabelle" and
wenzelm@62591	815	"isabelle_scala_script".
wenzelm@62591	816
wenzelm@63226	817	* Isabelle tools may consist of .scala files: the Scala compiler is
wenzelm@63226	818	invoked on the spot. The source needs to define some object that extends
wenzelm@63226	819	Isabelle_Tool.Body.
wenzelm@63226	820
wenzelm@62591	821	* The Isabelle ML process is now managed directly by Isabelle/Scala, and
wenzelm@62591	822	shell scripts merely provide optional command-line access. In
wenzelm@62591	823	particular:
wenzelm@62591	824
wenzelm@62591	825	. Scala module ML_Process to connect to the raw ML process,
wenzelm@62591	826	with interaction via stdin/stdout/stderr or in batch mode;
wenzelm@62591	827	. command-line tool "isabelle console" as interactive wrapper;
wenzelm@62591	828	. command-line tool "isabelle process" as batch mode wrapper.
wenzelm@62588	829
wenzelm@62588	830	* The executable "isabelle_process" has been discontinued. Tools and
wenzelm@62588	831	prover front-ends should use ML_Process or Isabelle_Process in
wenzelm@62591	832	Isabelle/Scala. INCOMPATIBILITY.
wenzelm@62588	833
wenzelm@62588	834	* New command-line tool "isabelle process" supports ML evaluation of
wenzelm@62588	835	literal expressions (option -e) or files (option -f) in the context of a
wenzelm@62588	836	given heap image. Errors lead to premature exit of the ML process with
wenzelm@62588	837	return code 1.
wenzelm@62588	838
wenzelm@62588	839	* Command-line tool "isabelle console" provides option -r to help to
wenzelm@62588	840	bootstrapping Isabelle/Pure interactively.
wenzelm@62588	841
wenzelm@62588	842	* Command-line tool "isabelle yxml" has been discontinued.
wenzelm@62588	843	INCOMPATIBILITY, use operations from the modules "XML" and "YXML" in
wenzelm@62588	844	Isabelle/ML or Isabelle/Scala.
wenzelm@62588	845
wenzelm@62549	846	* File.bash_string, File.bash_path etc. represent Isabelle/ML and
wenzelm@62549	847	Isabelle/Scala strings authentically within GNU bash. This is useful to
wenzelm@62549	848	produce robust shell scripts under program control, without worrying
wenzelm@62549	849	about spaces or special characters. Note that user output works via
wenzelm@62549	850	Path.print (ML) or Path.toString (Scala). INCOMPATIBILITY, the old (and
wenzelm@62549	851	less versatile) operations File.shell_quote, File.shell_path etc. have
wenzelm@62549	852	been discontinued.
wenzelm@62549	853
wenzelm@62591	854	* SML/NJ and old versions of Poly/ML are no longer supported.
wenzelm@62591	855
wenzelm@62642	856	* Poly/ML heaps now follow the hierarchy of sessions, and thus require
wenzelm@62642	857	much less disk space.
wenzelm@62642	858
wenzelm@62354	859
wenzelm@62354	860
wenzelm@62031	861	New in Isabelle2016 (February 2016)
wenzelm@62016	862	-----------------------------------
wenzelm@60138	863
wenzelm@61337	864	* General *
wenzelm@61337	865
wenzelm@62168	866	* Eisbach is now based on Pure instead of HOL. Objects-logics may import
wenzelm@62168	867	either the theory ~~/src/HOL/Eisbach/Eisbach (for HOL etc.) or
wenzelm@62168	868	~~/src/HOL/Eisbach/Eisbach_Old_Appl_Syntax (for FOL, ZF etc.). Note that
wenzelm@62168	869	the HOL-Eisbach session located in ~~/src/HOL/Eisbach/ contains further
wenzelm@62168	870	examples that do require HOL.
wenzelm@62168	871
wenzelm@62157	872	* Better resource usage on all platforms (Linux, Windows, Mac OS X) for
wenzelm@62157	873	both Isabelle/ML and Isabelle/Scala. Slightly reduced heap space usage.
wenzelm@62157	874
wenzelm@62017	875	* Former "xsymbols" syntax with Isabelle symbols is used by default,
wenzelm@62017	876	without any special print mode. Important ASCII replacement syntax
wenzelm@62017	877	remains available under print mode "ASCII", but less important syntax
wenzelm@62017	878	has been removed (see below).
wenzelm@62017	879
wenzelm@62109	880	* Support for more arrow symbols, with rendering in LaTeX and Isabelle
wenzelm@62109	881	fonts: \<Lleftarrow> \<Rrightarrow> \<longlongleftarrow> \<longlongrightarrow> \<longlonglongleftarrow> \<longlonglongrightarrow>.
wenzelm@62017	882
wenzelm@62108	883	* Special notation \<struct> for the first implicit 'structure' in the
wenzelm@62108	884	context has been discontinued. Rare INCOMPATIBILITY, use explicit
wenzelm@62108	885	structure name instead, notably in indexed notation with block-subscript
wenzelm@62108	886	(e.g. \<odot>\<^bsub>A\<^esub>).
wenzelm@62108	887
wenzelm@62108	888	* The glyph for \<diamond> in the IsabelleText font now corresponds better to its
wenzelm@62108	889	counterpart \<box> as quantifier-like symbol. A small diamond is available as
wenzelm@62108	890	\<diamondop>; the old symbol \<struct> loses this rendering and any special
wenzelm@62108	891	meaning.
wenzelm@62108	892
wenzelm@62017	893	* Syntax for formal comments "-- text" now also supports the symbolic
wenzelm@62017	894	form "\<comment> text". Command-line tool "isabelle update_cartouches -c" helps
wenzelm@62017	895	to update old sources.
wenzelm@62017	896
wenzelm@61337	897	* Toplevel theorem statements have been simplified as follows:
wenzelm@61337	898
wenzelm@61337	899	theorems ~> lemmas
wenzelm@61337	900	schematic_lemma ~> schematic_goal
wenzelm@61337	901	schematic_theorem ~> schematic_goal
wenzelm@61337	902	schematic_corollary ~> schematic_goal
wenzelm@61337	903
wenzelm@61337	904	Command-line tool "isabelle update_theorems" updates theory sources
wenzelm@61337	905	accordingly.
wenzelm@61337	906
wenzelm@61338	907	* Toplevel theorem statement 'proposition' is another alias for
wenzelm@61338	908	'theorem'.
wenzelm@61338	909
wenzelm@62169	910	* The old 'defs' command has been removed (legacy since Isabelle2014).
wenzelm@62169	911	INCOMPATIBILITY, use regular 'definition' instead. Overloaded and/or
wenzelm@62169	912	deferred definitions require a surrounding 'overloading' block.
wenzelm@62169	913
wenzelm@61337	914
wenzelm@60610	915	* Prover IDE -- Isabelle/Scala/jEdit *
wenzelm@60610	916
wenzelm@60986	917	* IDE support for the source-level debugger of Poly/ML, to work with
wenzelm@62253	918	Isabelle/ML and official Standard ML. Option "ML_debugger" and commands
wenzelm@62253	919	'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
wenzelm@62253	920	'SML_file_no_debug' control compilation of sources with or without
wenzelm@62253	921	debugging information. The Debugger panel allows to set breakpoints (via
wenzelm@62253	922	context menu), step through stopped threads, evaluate local ML
wenzelm@62253	923	expressions etc. At least one Debugger view needs to be active to have
wenzelm@62253	924	any effect on the running ML program.
wenzelm@60984	925
wenzelm@61803	926	* The State panel manages explicit proof state output, with dynamic
wenzelm@61803	927	auto-update according to cursor movement. Alternatively, the jEdit
wenzelm@61803	928	action "isabelle.update-state" (shortcut S+ENTER) triggers manual
wenzelm@61803	929	update.
wenzelm@61729	930
wenzelm@61729	931	* The Output panel no longer shows proof state output by default, to
wenzelm@61729	932	avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
wenzelm@61729	933	enable option "editor_output_state".
wenzelm@61215	934
wenzelm@61803	935	* The text overview column (status of errors, warnings etc.) is updated
wenzelm@61803	936	asynchronously, leading to much better editor reactivity. Moreover, the
wenzelm@61803	937	full document node content is taken into account. The width of the
wenzelm@61803	938	column is scaled according to the main text area font, for improved
wenzelm@61803	939	visibility.
wenzelm@61803	940
wenzelm@61803	941	* The main text area no longer changes its color hue in outdated
wenzelm@61803	942	situations. The text overview column takes over the role to indicate
wenzelm@61803	943	unfinished edits in the PIDE pipeline. This avoids flashing text display
wenzelm@61803	944	due to ad-hoc updates by auxiliary GUI components, such as the State
wenzelm@61803	945	panel.
wenzelm@61803	946
wenzelm@62254	947	* Slightly improved scheduling for urgent print tasks (e.g. command
wenzelm@62254	948	state output, interactive queries) wrt. long-running background tasks.
wenzelm@62017	949
wenzelm@62017	950	* Completion of symbols via prefix of \<name> or \<^name> or \name is
wenzelm@62017	951	always possible, independently of the language context. It is never
wenzelm@62017	952	implicit: a popup will show up unconditionally.
wenzelm@62017	953
wenzelm@62017	954	* Additional abbreviations for syntactic completion may be specified in
wenzelm@62017	955	$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
wenzelm@62017	956	support for simple templates using ASCII 007 (bell) as placeholder.
wenzelm@62017	957
wenzelm@62234	958	* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for
wenzelm@62234	959	completion like "+o", "*o", ".o" etc. -- due to conflicts with other
wenzelm@62234	960	ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
wenzelm@62234	961	suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
wenzelm@62234	962
wenzelm@61483	963	* Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
wenzelm@61483	964	emphasized text style; the effect is visible in document output, not in
wenzelm@61483	965	the editor.
wenzelm@61483	966
wenzelm@61483	967	* Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
wenzelm@61483	968	instead of former C+e LEFT.
wenzelm@61483	969
wenzelm@61512	970	* The command-line tool "isabelle jedit" and the isabelle.Main
wenzelm@62027	971	application wrapper treat the default $USER_HOME/Scratch.thy more
wenzelm@61512	972	uniformly, and allow the dummy file argument ":" to open an empty buffer
wenzelm@61512	973	instead.
wenzelm@61512	974
wenzelm@62017	975	* New command-line tool "isabelle jedit_client" allows to connect to an
wenzelm@62017	976	already running Isabelle/jEdit process. This achieves the effect of
wenzelm@62017	977	single-instance applications seen on common GUI desktops.
wenzelm@62017	978
wenzelm@61529	979	* The default look-and-feel for Linux is the traditional "Metal", which
wenzelm@61529	980	works better with GUI scaling for very high-resolution displays (e.g.
wenzelm@61529	981	4K). Moreover, it is generally more robust than "Nimbus".
wenzelm@61529	982
wenzelm@62163	983	* Update to jedit-5.3.0, with improved GUI scaling and support of
wenzelm@62163	984	high-resolution displays (e.g. 4K).
wenzelm@62163	985
wenzelm@62034	986	* The main Isabelle executable is managed as single-instance Desktop
wenzelm@62034	987	application uniformly on all platforms: Linux, Windows, Mac OS X.
wenzelm@62034	988
wenzelm@60610	989
wenzelm@61405	990	* Document preparation *
wenzelm@61405	991
haftmann@63553	992	* Text and ML antiquotation @{locale} for locales, similar to existing
haftmann@63553	993	antiquotations for classes.
haftmann@63553	994
wenzelm@62017	995	* Commands 'paragraph' and 'subparagraph' provide additional section
wenzelm@62017	996	headings. Thus there are 6 levels of standard headings, as in HTML.
wenzelm@62017	997
wenzelm@62017	998	* Command 'text_raw' has been clarified: input text is processed as in
wenzelm@62017	999	'text' (with antiquotations and control symbols). The key difference is
wenzelm@62017	1000	the lack of the surrounding isabelle markup environment in output.
wenzelm@62017	1001
wenzelm@62017	1002	* Text is structured in paragraphs and nested lists, using notation that
wenzelm@62017	1003	is similar to Markdown. The control symbols for list items are as
wenzelm@62017	1004	follows:
wenzelm@62017	1005
wenzelm@62017	1006	\<^item> itemize
wenzelm@62017	1007	\<^enum> enumerate
wenzelm@62017	1008	\<^descr> description
wenzelm@62017	1009
wenzelm@61491	1010	* There is a new short form for antiquotations with a single argument
wenzelm@61491	1011	that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
wenzelm@61595	1012	\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
wenzelm@61595	1013	\<^name> without following cartouche is equivalent to @{name}. The
wenzelm@61501	1014	standard Isabelle fonts provide glyphs to render important control
wenzelm@61501	1015	symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
wenzelm@61491	1016
wenzelm@61595	1017	* Antiquotations @{noindent}, @{smallskip}, @{medskip}, @{bigskip} with
wenzelm@61595	1018	corresponding control symbols \<^noindent>, \<^smallskip>, \<^medskip>, \<^bigskip> specify spacing formally, using
wenzelm@61595	1019	standard LaTeX macros of the same names.
wenzelm@61595	1020
wenzelm@61491	1021	* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
wenzelm@61491	1022	Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
wenzelm@61492	1023	text. Command-line tool "isabelle update_cartouches -t" helps to update
wenzelm@61492	1024	old sources, by approximative patching of the content of string and
wenzelm@61492	1025	cartouche tokens seen in theory sources.
wenzelm@61491	1026
wenzelm@61491	1027	* The @{text} antiquotation now ignores the antiquotation option
wenzelm@61491	1028	"source". The given text content is output unconditionally, without any
wenzelm@61491	1029	surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
wenzelm@61494	1030	argument where they are really intended, e.g. @{text \<open>"foo"\<close>}. Initial
wenzelm@61494	1031	or terminal spaces are ignored.
wenzelm@61491	1032
wenzelm@62017	1033	* Antiquotations @{emph} and @{bold} output LaTeX source recursively,
wenzelm@62017	1034	adding appropriate text style markup. These may be used in the short
wenzelm@62017	1035	form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
wenzelm@62017	1036
wenzelm@62017	1037	* Document antiquotation @{footnote} outputs LaTeX source recursively,
wenzelm@62017	1038	marked as \footnote{}. This may be used in the short form \<^footnote>\<open>...\<close>.
wenzelm@62017	1039
wenzelm@62017	1040	* Antiquotation @{verbatim [display]} supports option "indent".
wenzelm@62017	1041
wenzelm@62017	1042	* Antiquotation @{theory_text} prints uninterpreted theory source text
wenzelm@62231	1043	(Isar outer syntax with command keywords etc.). This may be used in the
wenzelm@62231	1044	short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".
wenzelm@62017	1045
wenzelm@62017	1046	* Antiquotation @{doc ENTRY} provides a reference to the given
wenzelm@62017	1047	documentation, with a hyperlink in the Prover IDE.
wenzelm@62017	1048
wenzelm@62017	1049	* Antiquotations @{command}, @{method}, @{attribute} print checked
wenzelm@62017	1050	entities of the Isar language.
wenzelm@62017	1051
wenzelm@61471	1052	* HTML presentation uses the standard IsabelleText font and Unicode
wenzelm@61471	1053	rendering of Isabelle symbols like Isabelle/Scala/jEdit. The former
wenzelm@61488	1054	print mode "HTML" loses its special meaning.
wenzelm@61471	1055
wenzelm@61405	1056
wenzelm@60406	1057	* Isar *
wenzelm@60406	1058
wenzelm@62205	1059	* Local goals ('have', 'show', 'hence', 'thus') allow structured rule
wenzelm@62205	1060	statements like fixes/assumes/shows in theorem specifications, but the
wenzelm@62205	1061	notation is postfix with keywords 'if' (or 'when') and 'for'. For
wenzelm@60555	1062	example:
wenzelm@60414	1063
wenzelm@60414	1064	have result: "C x y"
wenzelm@60414	1065	if "A x" and "B y"
wenzelm@60414	1066	for x :: 'a and y :: 'a
wenzelm@60414	1067	<proof>
wenzelm@60414	1068
wenzelm@60449	1069	The local assumptions are bound to the name "that". The result is
wenzelm@60449	1070	exported from context of the statement as usual. The above roughly
wenzelm@60414	1071	corresponds to a raw proof block like this:
wenzelm@60414	1072
wenzelm@60414	1073	{
wenzelm@60414	1074	fix x :: 'a and y :: 'a
wenzelm@60449	1075	assume that: "A x" "B y"
wenzelm@60414	1076	have "C x y" <proof>
wenzelm@60414	1077	}
wenzelm@60414	1078	note result = this
wenzelm@60406	1079
wenzelm@60555	1080	The keyword 'when' may be used instead of 'if', to indicate 'presume'
wenzelm@60555	1081	instead of 'assume' above.
wenzelm@60555	1082
wenzelm@61733	1083	* Assumptions ('assume', 'presume') allow structured rule statements
wenzelm@61733	1084	using 'if' and 'for', similar to 'have' etc. above. For example:
wenzelm@61658	1085
wenzelm@61658	1086	assume result: "C x y"
wenzelm@61658	1087	if "A x" and "B y"
wenzelm@61658	1088	for x :: 'a and y :: 'a
wenzelm@61658	1089
wenzelm@61658	1090	This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general
wenzelm@61658	1091	result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".
wenzelm@61658	1092
wenzelm@61658	1093	Vacuous quantification in assumptions is omitted, i.e. a for-context
wenzelm@61658	1094	only effects propositions according to actual use of variables. For
wenzelm@61658	1095	example:
wenzelm@61658	1096
wenzelm@61658	1097	assume "A x" and "B y" for x and y
wenzelm@61658	1098
wenzelm@61658	1099	is equivalent to:
wenzelm@61658	1100
wenzelm@61658	1101	assume "\<And>x. A x" and "\<And>y. B y"
wenzelm@61658	1102
wenzelm@60595	1103	* The meaning of 'show' with Pure rule statements has changed: premises
wenzelm@60595	1104	are treated in the sense of 'assume', instead of 'presume'. This means,
wenzelm@62205	1105	a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as
wenzelm@62205	1106	follows:
wenzelm@60595	1107
wenzelm@60595	1108	show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
wenzelm@60595	1109
wenzelm@60595	1110	or:
wenzelm@60595	1111
wenzelm@60595	1112	show "C x" if "A x" "B x" for x
wenzelm@60595	1113
wenzelm@60595	1114	Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:
wenzelm@60595	1115
wenzelm@60595	1116	show "C x" when "A x" "B x" for x
wenzelm@60595	1117
wenzelm@60459	1118	* New command 'consider' states rules for generalized elimination and
wenzelm@60459	1119	case splitting. This is like a toplevel statement "theorem obtains" used
wenzelm@60459	1120	within a proof body; or like a multi-branch 'obtain' without activation
wenzelm@60459	1121	of the local context elements yet.
wenzelm@60459	1122
wenzelm@60455	1123	* Proof method "cases" allows to specify the rule as first entry of
wenzelm@60455	1124	chained facts. This is particularly useful with 'consider':
wenzelm@60455	1125
wenzelm@60455	1126	consider (a) A \| (b) B \| (c) C <proof>
wenzelm@60455	1127	then have something
wenzelm@60455	1128	proof cases
wenzelm@60455	1129	case a
wenzelm@60455	1130	then show ?thesis <proof>
wenzelm@60455	1131	next
wenzelm@60455	1132	case b
wenzelm@60455	1133	then show ?thesis <proof>
wenzelm@60455	1134	next
wenzelm@60455	1135	case c
wenzelm@60455	1136	then show ?thesis <proof>
wenzelm@60455	1137	qed
wenzelm@60455	1138
wenzelm@60565	1139	* Command 'case' allows fact name and attribute specification like this:
wenzelm@60565	1140
wenzelm@60565	1141	case a: (c xs)
wenzelm@60565	1142	case a [attributes]: (c xs)
wenzelm@60565	1143
wenzelm@60565	1144	Facts that are introduced by invoking the case context are uniformly
wenzelm@60565	1145	qualified by "a"; the same name is used for the cumulative fact. The old
wenzelm@60565	1146	form "case (c xs) [attributes]" is no longer supported. Rare
wenzelm@60565	1147	INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
wenzelm@60565	1148	and always put attributes in front.
wenzelm@60565	1149
wenzelm@60618	1150	* The standard proof method of commands 'proof' and '..' is now called
wenzelm@60618	1151	"standard" to make semantically clear what it is; the old name "default"
wenzelm@60618	1152	is still available as legacy for some time. Documentation now explains
wenzelm@60618	1153	'..' more accurately as "by standard" instead of "by rule".
wenzelm@60618	1154
wenzelm@62017	1155	* Nesting of Isar goal structure has been clarified: the context after
wenzelm@62017	1156	the initial backwards refinement is retained for the whole proof, within
wenzelm@62017	1157	all its context sections (as indicated via 'next'). This is e.g.
wenzelm@62017	1158	relevant for 'using', 'including', 'supply':
wenzelm@62017	1159
wenzelm@62017	1160	have "A \<and> A" if a: A for A
wenzelm@62017	1161	supply [simp] = a
wenzelm@62017	1162	proof
wenzelm@62017	1163	show A by simp
wenzelm@62017	1164	next
wenzelm@62017	1165	show A by simp
wenzelm@62017	1166	qed
wenzelm@62017	1167
wenzelm@62017	1168	* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
wenzelm@62017	1169	proof body as well, abstracted over relevant parameters.
wenzelm@62017	1170
wenzelm@62017	1171	* Improved type-inference for theorem statement 'obtains': separate
wenzelm@62017	1172	parameter scope for of each clause.
wenzelm@62017	1173
wenzelm@62017	1174	* Term abbreviations via 'is' patterns also work for schematic
wenzelm@62017	1175	statements: result is abstracted over unknowns.
wenzelm@62017	1176
wenzelm@60631	1177	* Command 'subgoal' allows to impose some structure on backward
wenzelm@60631	1178	refinements, to avoid proof scripts degenerating into long of 'apply'
wenzelm@60631	1179	sequences. Further explanations and examples are given in the isar-ref
wenzelm@60631	1180	manual.
wenzelm@60631	1181
wenzelm@62017	1182	* Command 'supply' supports fact definitions during goal refinement
wenzelm@62017	1183	('apply' scripts).
wenzelm@62017	1184
wenzelm@61166	1185	* Proof method "goal_cases" turns the current subgoals into cases within
wenzelm@61166	1186	the context; the conclusion is bound to variable ?case in each case. For
wenzelm@61166	1187	example:
wenzelm@60617	1188
wenzelm@60617	1189	lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
wenzelm@60622	1190	and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
wenzelm@61166	1191	proof goal_cases
wenzelm@60622	1192	case (1 x)
wenzelm@60622	1193	then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
wenzelm@60622	1194	next
wenzelm@60622	1195	case (2 y z)
wenzelm@60622	1196	then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
wenzelm@60622	1197	qed
wenzelm@60622	1198
wenzelm@60622	1199	lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
wenzelm@60622	1200	and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
wenzelm@61166	1201	proof goal_cases
wenzelm@60617	1202	case prems: 1
wenzelm@60617	1203	then show ?case using prems sorry
wenzelm@60617	1204	next
wenzelm@60617	1205	case prems: 2
wenzelm@60617	1206	then show ?case using prems sorry
wenzelm@60617	1207	qed
wenzelm@60578	1208
wenzelm@60581	1209	* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
wenzelm@60617	1210	is marked as legacy, and will be removed eventually. The proof method
wenzelm@60617	1211	"goals" achieves a similar effect within regular Isar; often it can be
wenzelm@60617	1212	done more adequately by other means (e.g. 'consider').
wenzelm@60581	1213
wenzelm@62017	1214	* The vacuous fact "TERM x" may be established "by fact" or as `TERM x`
wenzelm@62017	1215	as well, not just "by this" or "." as before.
wenzelm@60551	1216
wenzelm@60554	1217	* Method "sleep" succeeds after a real-time delay (in seconds). This is
wenzelm@60554	1218	occasionally useful for demonstration and testing purposes.
wenzelm@60554	1219
wenzelm@60406	1220
wenzelm@60331	1221	* Pure *
wenzelm@60331	1222
wenzelm@61606	1223	* Qualifiers in locale expressions default to mandatory ('!') regardless
wenzelm@61606	1224	of the command. Previously, for 'locale' and 'sublocale' the default was
wenzelm@61606	1225	optional ('?'). The old synatx '!' has been discontinued.
wenzelm@61606	1226	INCOMPATIBILITY, remove '!' and add '?' as required.
ballarin@61565	1227
ballarin@61566	1228	* Keyword 'rewrites' identifies rewrite morphisms in interpretation
wenzelm@62017	1229	commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
ballarin@61566	1230
ballarin@61701	1231	* More gentle suppression of syntax along locale morphisms while
wenzelm@62017	1232	printing terms. Previously 'abbreviation' and 'notation' declarations
wenzelm@62017	1233	would be suppressed for morphisms except term identity. Now
ballarin@61701	1234	'abbreviation' is also kept for morphims that only change the involved
wenzelm@62017	1235	parameters, and only 'notation' is suppressed. This can be of great help
wenzelm@62017	1236	when working with complex locale hierarchies, because proof states are
wenzelm@62017	1237	displayed much more succinctly. It also means that only notation needs
wenzelm@62017	1238	to be redeclared if desired, as illustrated by this example:
ballarin@61701	1239
ballarin@61701	1240	locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
ballarin@61701	1241	begin
ballarin@61701	1242	definition derived (infixl "\<odot>" 65) where ...
ballarin@61701	1243	end
ballarin@61701	1244
ballarin@61701	1245	locale morphism =
ballarin@61701	1246	left: struct composition + right: struct composition'
ballarin@61701	1247	for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
ballarin@61701	1248	begin
ballarin@61701	1249	notation right.derived ("\<odot>''")
ballarin@61701	1250	end
ballarin@61701	1251
wenzelm@61895	1252	* Command 'global_interpretation' issues interpretations into global
wenzelm@61895	1253	theories, with optional rewrite definitions following keyword 'defines'.
wenzelm@61895	1254
wenzelm@61895	1255	* Command 'sublocale' accepts optional rewrite definitions after keyword
haftmann@61675	1256	'defines'.
haftmann@61675	1257
wenzelm@61895	1258	* Command 'permanent_interpretation' has been discontinued. Use
wenzelm@61895	1259	'global_interpretation' or 'sublocale' instead. INCOMPATIBILITY.
haftmann@61670	1260
wenzelm@61252	1261	* Command 'print_definitions' prints dependencies of definitional
wenzelm@61252	1262	specifications. This functionality used to be part of 'print_theory'.
wenzelm@61252	1263
wenzelm@60331	1264	* Configuration option rule_insts_schematic has been discontinued
wenzelm@62017	1265	(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
wenzelm@60331	1266
wenzelm@62205	1267	* Abbreviations in type classes now carry proper sort constraint. Rare
wenzelm@62205	1268	INCOMPATIBILITY in situations where the previous misbehaviour has been
wenzelm@62205	1269	exploited.
haftmann@60347	1270
haftmann@60347	1271	* Refinement of user-space type system in type classes: pseudo-local
wenzelm@62205	1272	operations behave more similar to abbreviations. Potential
haftmann@60347	1273	INCOMPATIBILITY in exotic situations.
haftmann@60347	1274
haftmann@60347	1275
nipkow@60171	1276	* HOL *
nipkow@60171	1277
wenzelm@62017	1278	* The 'typedef' command has been upgraded from a partially checked
wenzelm@62017	1279	"axiomatization", to a full definitional specification that takes the
wenzelm@62017	1280	global collection of overloaded constant / type definitions into
wenzelm@62017	1281	account. Type definitions with open dependencies on overloaded
wenzelm@62017	1282	definitions need to be specified as "typedef (overloaded)". This
wenzelm@62017	1283	provides extra robustness in theory construction. Rare INCOMPATIBILITY.
wenzelm@62017	1284
wenzelm@62017	1285	* Qualification of various formal entities in the libraries is done more
wenzelm@62017	1286	uniformly via "context begin qualified definition ... end" instead of
wenzelm@62017	1287	old-style "hide_const (open) ...". Consequently, both the defined
wenzelm@62017	1288	constant and its defining fact become qualified, e.g. Option.is_none and
wenzelm@62017	1289	Option.is_none_def. Occasional INCOMPATIBILITY in applications.
wenzelm@62017	1290
wenzelm@62017	1291	* Some old and rarely used ASCII replacement syntax has been removed.
wenzelm@62017	1292	INCOMPATIBILITY, standard syntax with symbols should be used instead.
wenzelm@62017	1293	The subsequent commands help to reproduce the old forms, e.g. to
wenzelm@62017	1294	simplify porting old theories:
wenzelm@62017	1295
wenzelm@62017	1296	notation iff (infixr "<->" 25)
wenzelm@62017	1297
wenzelm@62017	1298	notation Times (infixr "<*>" 80)
wenzelm@62017	1299
wenzelm@62017	1300	type_notation Map.map (infixr "~=>" 0)
wenzelm@62017	1301	notation Map.map_comp (infixl "o'_m" 55)
wenzelm@62017	1302
wenzelm@62017	1303	type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
wenzelm@62017	1304
wenzelm@62017	1305	notation FuncSet.funcset (infixr "->" 60)
wenzelm@62017	1306	notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60)
wenzelm@62017	1307
wenzelm@62017	1308	notation Omega_Words_Fun.conc (infixr "conc" 65)
wenzelm@62017	1309
wenzelm@62017	1310	notation Preorder.equiv ("op ~~")
wenzelm@62017	1311	and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
wenzelm@62017	1312
wenzelm@62017	1313	notation (in topological_space) tendsto (infixr "--->" 55)
wenzelm@62017	1314	notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
wenzelm@62017	1315	notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
wenzelm@62017	1316
wenzelm@62017	1317	notation NSA.approx (infixl "@=" 50)
wenzelm@62017	1318	notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
wenzelm@62017	1319	notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
wenzelm@62017	1320
wenzelm@62017	1321	* The alternative notation "\<Colon>" for type and sort constraints has been
wenzelm@62017	1322	removed: in LaTeX document output it looks the same as "::".
wenzelm@62017	1323	INCOMPATIBILITY, use plain "::" instead.
wenzelm@62017	1324
wenzelm@62017	1325	* Commands 'inductive' and 'inductive_set' work better when names for
wenzelm@62017	1326	intro rules are omitted: the "cases" and "induct" rules no longer
wenzelm@62017	1327	declare empty case_names, but no case_names at all. This allows to use
wenzelm@62017	1328	numbered cases in proofs, without requiring method "goal_cases".
wenzelm@62017	1329
wenzelm@62017	1330	* Inductive definitions ('inductive', 'coinductive', etc.) expose
wenzelm@62017	1331	low-level facts of the internal construction only if the option
wenzelm@62093	1332	"inductive_internals" is enabled. This refers to the internal predicate
wenzelm@62017	1333	definition and its monotonicity result. Rare INCOMPATIBILITY.
wenzelm@62017	1334
wenzelm@62017	1335	* Recursive function definitions ('fun', 'function', 'partial_function')
wenzelm@62017	1336	expose low-level facts of the internal construction only if the option
wenzelm@62205	1337	"function_internals" is enabled. Its internal inductive definition is
wenzelm@62205	1338	also subject to "inductive_internals". Rare INCOMPATIBILITY.
wenzelm@62093	1339
wenzelm@62093	1340	* BNF datatypes ('datatype', 'codatatype', etc.) expose low-level facts
wenzelm@62093	1341	of the internal construction only if the option "bnf_internals" is
wenzelm@62093	1342	enabled. This supersedes the former option "bnf_note_all". Rare
wenzelm@62093	1343	INCOMPATIBILITY.
wenzelm@62017	1344
wenzelm@62017	1345	* Combinator to represent case distinction on products is named
wenzelm@62017	1346	"case_prod", uniformly, discontinuing any input aliasses. Very popular
wenzelm@62017	1347	theorem aliasses have been retained.
wenzelm@62017	1348
haftmann@61424	1349	Consolidated facts:
haftmann@61424	1350	PairE ~> prod.exhaust
haftmann@61424	1351	Pair_eq ~> prod.inject
haftmann@61424	1352	pair_collapse ~> prod.collapse
haftmann@61424	1353	Pair_fst_snd_eq ~> prod_eq_iff
haftmann@61424	1354	split_twice ~> prod.case_distrib
haftmann@61424	1355	split_weak_cong ~> prod.case_cong_weak
haftmann@61424	1356	split_split ~> prod.split
haftmann@61424	1357	split_split_asm ~> prod.split_asm
haftmann@61424	1358	splitI ~> case_prodI
haftmann@61424	1359	splitD ~> case_prodD
haftmann@61424	1360	splitI2 ~> case_prodI2
haftmann@61424	1361	splitI2' ~> case_prodI2'
haftmann@61424	1362	splitE ~> case_prodE
haftmann@61424	1363	splitE' ~> case_prodE'
haftmann@61424	1364	split_pair ~> case_prod_Pair
haftmann@61424	1365	split_eta ~> case_prod_eta
haftmann@61424	1366	split_comp ~> case_prod_comp
haftmann@61424	1367	mem_splitI ~> mem_case_prodI
haftmann@61424	1368	mem_splitI2 ~> mem_case_prodI2
haftmann@61424	1369	mem_splitE ~> mem_case_prodE
haftmann@61424	1370	The_split ~> The_case_prod
haftmann@61424	1371	cond_split_eta ~> cond_case_prod_eta
haftmann@61424	1372	Collect_split_in_rel_leE ~> Collect_case_prod_in_rel_leE
haftmann@61424	1373	Collect_split_in_rel_leI ~> Collect_case_prod_in_rel_leI
haftmann@61424	1374	in_rel_Collect_split_eq ~> in_rel_Collect_case_prod_eq
haftmann@61424	1375	Collect_split_Grp_eqD ~> Collect_case_prod_Grp_eqD
haftmann@61424	1376	Collect_split_Grp_inD ~> Collect_case_prod_Grp_in
haftmann@61424	1377	Domain_Collect_split ~> Domain_Collect_case_prod
haftmann@61424	1378	Image_Collect_split ~> Image_Collect_case_prod
haftmann@61424	1379	Range_Collect_split ~> Range_Collect_case_prod
haftmann@61424	1380	Eps_split ~> Eps_case_prod
haftmann@61424	1381	Eps_split_eq ~> Eps_case_prod_eq
haftmann@61424	1382	split_rsp ~> case_prod_rsp
haftmann@61424	1383	curry_split ~> curry_case_prod
haftmann@61424	1384	split_curry ~> case_prod_curry
wenzelm@62017	1385
haftmann@61424	1386	Changes in structure HOLogic:
haftmann@61424	1387	split_const ~> case_prod_const
haftmann@61424	1388	mk_split ~> mk_case_prod
haftmann@61424	1389	mk_psplits ~> mk_ptupleabs
haftmann@61424	1390	strip_psplits ~> strip_ptupleabs
wenzelm@62017	1391
wenzelm@62017	1392	INCOMPATIBILITY.
wenzelm@62017	1393
wenzelm@62017	1394	* The coercions to type 'real' have been reorganised. The function
wenzelm@62017	1395	'real' is no longer overloaded, but has type 'nat => real' and
wenzelm@62017	1396	abbreviates of_nat for that type. Also 'real_of_int :: int => real'
wenzelm@62017	1397	abbreviates of_int for that type. Other overloaded instances of 'real'
wenzelm@62017	1398	have been replaced by 'real_of_ereal' and 'real_of_float'.
wenzelm@62017	1399
lp15@61694	1400	Consolidated facts (among others):
lp15@61694	1401	real_of_nat_le_iff -> of_nat_le_iff
lp15@61694	1402	real_of_nat_numeral of_nat_numeral
lp15@61694	1403	real_of_int_zero of_int_0
lp15@61694	1404	real_of_nat_zero of_nat_0
lp15@61694	1405	real_of_one of_int_1
lp15@61694	1406	real_of_int_add of_int_add
lp15@61694	1407	real_of_nat_add of_nat_add
lp15@61694	1408	real_of_int_diff of_int_diff
lp15@61694	1409	real_of_nat_diff of_nat_diff
lp15@61694	1410	floor_subtract floor_diff_of_int
lp15@61694	1411	real_of_int_inject of_int_eq_iff
lp15@61694	1412	real_of_int_gt_zero_cancel_iff of_int_0_less_iff
lp15@61694	1413	real_of_int_ge_zero_cancel_iff of_int_0_le_iff
lp15@61694	1414	real_of_nat_ge_zero of_nat_0_le_iff
lp15@61694	1415	real_of_int_ceiling_ge le_of_int_ceiling
lp15@61694	1416	ceiling_less_eq ceiling_less_iff
lp15@61694	1417	ceiling_le_eq ceiling_le_iff
lp15@61694	1418	less_floor_eq less_floor_iff
lp15@61694	1419	floor_less_eq floor_less_iff
lp15@61694	1420	floor_divide_eq_div floor_divide_of_int_eq
lp15@61694	1421	real_of_int_zero_cancel of_nat_eq_0_iff
lp15@61694	1422	ceiling_real_of_int ceiling_of_int
wenzelm@62017	1423
wenzelm@62017	1424	INCOMPATIBILITY.
wenzelm@61143	1425
wenzelm@60841	1426	* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
wenzelm@60841	1427	been removed. INCOMPATIBILITY.
wenzelm@60841	1428
lars@60712	1429	* Quickcheck setup for finite sets.
lars@60712	1430
nipkow@60171	1431	* Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
wenzelm@60138	1432
blanchet@60306	1433	* Sledgehammer:
blanchet@61318	1434	- The MaSh relevance filter has been sped up.
blanchet@60306	1435	- Proof reconstruction has been improved, to minimize the incidence of
blanchet@60306	1436	cases where Sledgehammer gives a proof that does not work.
blanchet@60306	1437	- Auto Sledgehammer now minimizes and preplays the results.
blanchet@61030	1438	- Handle Vampire 4.0 proof output without raising exception.
blanchet@61043	1439	- Eliminated "MASH" environment variable. Use the "MaSh" option in
blanchet@61043	1440	Isabelle/jEdit instead. INCOMPATIBILITY.
blanchet@61317	1441	- Eliminated obsolete "blocking" option and related subcommands.
blanchet@60306	1442
blanchet@60310	1443	* Nitpick:
blanchet@61325	1444	- Fixed soundness bug in translation of "finite" predicate.
blanchet@61324	1445	- Fixed soundness bug in "destroy_constrs" optimization.
blanchet@62080	1446	- Fixed soundness bug in translation of "rat" type.
blanchet@60310	1447	- Removed "check_potential" and "check_genuine" options.
blanchet@61317	1448	- Eliminated obsolete "blocking" option.
blanchet@60310	1449
wenzelm@62027	1450	* (Co)datatype package:
blanchet@61345	1451	- New commands "lift_bnf" and "copy_bnf" for lifting (copying) a BNF
blanchet@61345	1452	structure on the raw type to an abstract type defined using typedef.
blanchet@61345	1453	- Always generate "case_transfer" theorem.
wenzelm@62235	1454	- For mutual types, generate slightly stronger "rel_induct",
wenzelm@62235	1455	"rel_coinduct", and "coinduct" theorems. INCOMPATIBLITY.
blanchet@61551	1456	- Allow discriminators and selectors with the same name as the type
blanchet@61551	1457	being defined.
blanchet@61551	1458	- Avoid various internal name clashes (e.g., 'datatype f = f').
traytel@60920	1459
wenzelm@62098	1460	* Transfer: new methods for interactive debugging of 'transfer' and
wenzelm@62098	1461	'transfer_prover': 'transfer_start', 'transfer_step', 'transfer_end',
wenzelm@62098	1462	'transfer_prover_start' and 'transfer_prover_end'.
kuncar@61370	1463
kleing@62118	1464	* New diagnostic command print_record for displaying record definitions.
kleing@62118	1465
haftmann@60868	1466	* Division on integers is bootstrapped directly from division on
wenzelm@62017	1467	naturals and uses generic numeral algorithm for computations. Slight
wenzelm@62017	1468	INCOMPATIBILITY, simproc numeral_divmod replaces and generalizes former
wenzelm@62017	1469	simprocs binary_int_div and binary_int_mod
wenzelm@62017	1470
wenzelm@62017	1471	* Tightened specification of class semiring_no_zero_divisors. Minor
haftmann@60516	1472	INCOMPATIBILITY.
haftmann@60516	1473
haftmann@60688	1474	* Class algebraic_semidom introduces common algebraic notions of
wenzelm@62017	1475	integral (semi)domains, particularly units. Although logically subsumed
wenzelm@62017	1476	by fields, is is not a super class of these in order not to burden
wenzelm@62017	1477	fields with notions that are trivial there.
wenzelm@62017	1478
wenzelm@62017	1479	* Class normalization_semidom specifies canonical representants for
wenzelm@62017	1480	equivalence classes of associated elements in an integral (semi)domain.
wenzelm@62017	1481	This formalizes associated elements as well.
haftmann@60688	1482
haftmann@60688	1483	* Abstract specification of gcd/lcm operations in classes semiring_gcd,
wenzelm@62017	1484	semiring_Gcd, semiring_Lcd. Minor INCOMPATIBILITY: facts gcd_nat.commute
wenzelm@62017	1485	and gcd_int.commute are subsumed by gcd.commute, as well as
wenzelm@62017	1486	gcd_nat.assoc and gcd_int.assoc by gcd.assoc.
wenzelm@62017	1487
wenzelm@62017	1488	* Former constants Fields.divide (_ / _) and Divides.div (_ div _) are
wenzelm@62017	1489	logically unified to Rings.divide in syntactic type class Rings.divide,
wenzelm@62017	1490	with infix syntax (_ div _). Infix syntax (_ / _) for field division is
wenzelm@62017	1491	added later as abbreviation in class Fields.inverse. INCOMPATIBILITY,
wenzelm@62017	1492	instantiations must refer to Rings.divide rather than the former
wenzelm@62017	1493	separate constants, hence infix syntax (_ / _) is usually not available
wenzelm@62017	1494	during instantiation.
wenzelm@62017	1495
wenzelm@62017	1496	* New cancellation simprocs for boolean algebras to cancel complementary
wenzelm@62017	1497	terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
wenzelm@62017	1498	"top". INCOMPATIBILITY.
Andreas@61629	1499
hoelzl@62101	1500	* Class uniform_space introduces uniform spaces btw topological spaces
hoelzl@62101	1501	and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
wenzelm@62205	1502	introduced in the form of an uniformity. Some constants are more general
wenzelm@62205	1503	now, it may be necessary to add type class constraints.
hoelzl@62101	1504
hoelzl@62101	1505	open_real_def \<leadsto> open_dist
hoelzl@62101	1506	open_complex_def \<leadsto> open_dist
hoelzl@62101	1507
wenzelm@62026	1508	* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
wenzelm@62026	1509
Mathias@60397	1510	* Library/Multiset:
Mathias@60397	1511	- Renamed multiset inclusion operators:
Mathias@60397	1512	< ~> <#
blanchet@62208	1513	> ~> >#
Mathias@60397	1514	<= ~> <=#
blanchet@62208	1515	>= ~> >=#
Mathias@60397	1516	\<le> ~> \<le>#
blanchet@62208	1517	\<ge> ~> \<ge>#
Mathias@60397	1518	INCOMPATIBILITY.
blanchet@62209	1519	- Added multiset inclusion operator syntax:
blanchet@62209	1520	\<subset>#
blanchet@62209	1521	\<subseteq>#
blanchet@62209	1522	\<supset>#
blanchet@62209	1523	\<supseteq>#
Mathias@60397	1524	- "'a multiset" is no longer an instance of the "order",
Mathias@60397	1525	"ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
Mathias@60397	1526	"semilattice_inf", and "semilattice_sup" type classes. The theorems
Mathias@60397	1527	previously provided by these type classes (directly or indirectly)
Mathias@60397	1528	are now available through the "subset_mset" interpretation
Mathias@60397	1529	(e.g. add_mono ~> subset_mset.add_mono).
Mathias@60397	1530	INCOMPATIBILITY.
nipkow@60497	1531	- Renamed conversions:
nipkow@60515	1532	multiset_of ~> mset
nipkow@60515	1533	multiset_of_set ~> mset_set
nipkow@60497	1534	set_of ~> set_mset
nipkow@60497	1535	INCOMPATIBILITY
Mathias@60398	1536	- Renamed lemmas:
Mathias@60398	1537	mset_le_def ~> subseteq_mset_def
Mathias@60398	1538	mset_less_def ~> subset_mset_def
Mathias@60400	1539	less_eq_multiset.rep_eq ~> subseteq_mset_def
Mathias@60400	1540	INCOMPATIBILITY
Mathias@60400	1541	- Removed lemmas generated by lift_definition:
wenzelm@62235	1542	less_eq_multiset.abs_eq, less_eq_multiset.rsp,
wenzelm@62235	1543	less_eq_multiset.transfer, less_eq_multiset_def
Mathias@60400	1544	INCOMPATIBILITY
wenzelm@60006	1545
wenzelm@62017	1546	* Library/Omega_Words_Fun: Infinite words modeled as functions nat \<Rightarrow> 'a.
wenzelm@62017	1547
wenzelm@62017	1548	* Library/Bourbaki_Witt_Fixpoint: Added formalisation of the
wenzelm@62017	1549	Bourbaki-Witt fixpoint theorem for increasing functions in
wenzelm@62017	1550	chain-complete partial orders.
wenzelm@62017	1551
wenzelm@62017	1552	* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
wenzelm@62017	1553	Minor INCOMPATIBILITY, use 'function' instead.
wenzelm@62017	1554
wenzelm@62064	1555	* Library/Periodic_Fun: a locale that provides convenient lemmas for
wenzelm@62064	1556	periodic functions.
eberlm@62060	1557
wenzelm@62098	1558	* Library/Formal_Power_Series: proper definition of division (with
wenzelm@62098	1559	remainder) for formal power series; instances for Euclidean Ring and
wenzelm@62098	1560	GCD.
eberlm@62086	1561
wenzelm@62084	1562	* HOL-Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
wenzelm@62084	1563
wenzelm@62084	1564	* HOL-Statespace: command 'statespace' uses mandatory qualifier for
wenzelm@62084	1565	import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
wenzelm@62084	1566	remove '!' and add '?' as required.
wenzelm@62084	1567
wenzelm@62237	1568	* HOL-Decision_Procs: The "approximation" method works with "powr"
wenzelm@62237	1569	(exponentiation on real numbers) again.
wenzelm@62237	1570
wenzelm@62084	1571	* HOL-Multivariate_Analysis: theory Cauchy_Integral_Thm with Contour
wenzelm@62084	1572	integrals (= complex path integrals), Cauchy's integral theorem, winding
wenzelm@62084	1573	numbers and Cauchy's integral formula, Liouville theorem, Fundamental
wenzelm@62084	1574	Theorem of Algebra. Ported from HOL Light.
wenzelm@62084	1575
wenzelm@62084	1576	* HOL-Multivariate_Analysis: topological concepts such as connected
wenzelm@62017	1577	components, homotopic paths and the inside or outside of a set.
wenzelm@61121	1578
wenzelm@62084	1579	* HOL-Multivariate_Analysis: radius of convergence of power series and
wenzelm@62064	1580	various summability tests; Harmonic numbers and the Euler–Mascheroni
wenzelm@62064	1581	constant; the Generalised Binomial Theorem; the complex and real
wenzelm@62064	1582	Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
wenzelm@62064	1583	properties.
eberlm@62060	1584
wenzelm@62084	1585	* HOL-Probability: The central limit theorem based on Levy's uniqueness
wenzelm@62084	1586	and continuity theorems, weak convergence, and characterisitc functions.
wenzelm@62084	1587
wenzelm@62084	1588	* HOL-Data_Structures: new and growing session of standard data
wenzelm@62084	1589	structures.
lammich@61178	1590
wenzelm@60479	1591
wenzelm@60793	1592	* ML *
wenzelm@60793	1593
wenzelm@62017	1594	* The following combinators for low-level profiling of the ML runtime
wenzelm@62017	1595	system are available:
wenzelm@62017	1596
wenzelm@62017	1597	profile_time (CPU time)
wenzelm@62017	1598	profile_time_thread (CPU time on this thread)
wenzelm@62017	1599	profile_allocations (overall heap allocations)
wenzelm@62017	1600
wenzelm@62017	1601	* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
wenzelm@62017	1602
wenzelm@62075	1603	* Antiquotation @{method NAME} inlines the (checked) name of the given
wenzelm@62075	1604	Isar proof method.
wenzelm@62075	1605
wenzelm@61922	1606	* Pretty printing of Poly/ML compiler output in Isabelle has been
wenzelm@61922	1607	improved: proper treatment of break offsets and blocks with consistent
wenzelm@61922	1608	breaks.
wenzelm@61922	1609
wenzelm@61268	1610	* The auxiliary module Pure/display.ML has been eliminated. Its
wenzelm@61268	1611	elementary thm print operations are now in Pure/more_thm.ML and thus
wenzelm@61268	1612	called Thm.pretty_thm, Thm.string_of_thm etc. INCOMPATIBILITY.
wenzelm@61268	1613
wenzelm@61144	1614	* Simproc programming interfaces have been simplified:
wenzelm@61144	1615	Simplifier.make_simproc and Simplifier.define_simproc supersede various
wenzelm@61144	1616	forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
wenzelm@61144	1617	term patterns for the left-hand sides are specified with implicitly
wenzelm@61144	1618	fixed variables, like top-level theorem statements. INCOMPATIBILITY.
wenzelm@61144	1619
wenzelm@60802	1620	* Instantiation rules have been re-organized as follows:
wenzelm@60802	1621
wenzelm@60802	1622	Thm.instantiate (low-level instantiation with named arguments)
wenzelm@60802	1623	Thm.instantiate' (version with positional arguments)
wenzelm@60802	1624
wenzelm@60802	1625	Drule.infer_instantiate (instantiation with type inference)
wenzelm@60802	1626	Drule.infer_instantiate' (version with positional arguments)
wenzelm@60802	1627
wenzelm@60802	1628	The LHS only requires variable specifications, instead of full terms.
wenzelm@60802	1629	Old cterm_instantiate is superseded by infer_instantiate.
wenzelm@60802	1630	INCOMPATIBILITY, need to re-adjust some ML names and types accordingly.
wenzelm@60802	1631
wenzelm@60793	1632	* Old tactic shorthands atac, rtac, etac, dtac, ftac have been
wenzelm@60793	1633	discontinued. INCOMPATIBILITY, use regular assume_tac, resolve_tac etc.
wenzelm@60793	1634	instead (with proper context).
wenzelm@60642	1635
wenzelm@60642	1636	* Thm.instantiate (and derivatives) no longer require the LHS of the
wenzelm@60642	1637	instantiation to be certified: plain variables are given directly.
wenzelm@60642	1638
wenzelm@60707	1639	* Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous
wenzelm@60707	1640	quasi-bound variables (like the Simplifier), instead of accidentally
wenzelm@60707	1641	named local fixes. This has the potential to improve stability of proof
wenzelm@60707	1642	tools, but can also cause INCOMPATIBILITY for tools that don't observe
wenzelm@60707	1643	the proof context discipline.
wenzelm@60707	1644
wenzelm@62017	1645	* Isar proof methods are based on a slightly more general type
wenzelm@62017	1646	context_tactic, which allows to change the proof context dynamically
wenzelm@62017	1647	(e.g. to update cases) and indicate explicit Seq.Error results. Former
wenzelm@62017	1648	METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
wenzelm@62017	1649	provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
wenzelm@61885	1650
wenzelm@60642	1651
wenzelm@60983	1652	* System *
wenzelm@60983	1653
wenzelm@62525	1654	* Command-line tool "isabelle console" enables print mode "ASCII".
wenzelm@61958	1655
wenzelm@62017	1656	* Command-line tool "isabelle update_then" expands old Isar command
wenzelm@62017	1657	conflations:
wenzelm@62017	1658
wenzelm@62017	1659	hence ~> then have
wenzelm@62017	1660	thus ~> then show
wenzelm@62017	1661
wenzelm@62017	1662	This syntax is more orthogonal and improves readability and
wenzelm@62017	1663	maintainability of proofs.
wenzelm@62017	1664
wenzelm@61602	1665	* Global session timeout is multiplied by timeout_scale factor. This
wenzelm@61602	1666	allows to adjust large-scale tests (e.g. AFP) to overall hardware
wenzelm@61602	1667	performance.
wenzelm@61602	1668
wenzelm@61174	1669	* Property values in etc/symbols may contain spaces, if written with the
wenzelm@62671	1670	replacement character "␣" (Unicode point 0x2324). For example:
wenzelm@62671	1671
wenzelm@62671	1672	\<star> code: 0x0022c6 group: operator font: Deja␣Vu␣Sans␣Mono
wenzelm@61174	1673
wenzelm@60995	1674	* Java runtime environment for x86_64-windows allows to use larger heap
wenzelm@60995	1675	space.
wenzelm@60995	1676
wenzelm@61135	1677	* Java runtime options are determined separately for 32bit vs. 64bit
wenzelm@61135	1678	platforms as follows.
wenzelm@61135	1679
wenzelm@61135	1680	- Isabelle desktop application: platform-specific files that are
wenzelm@61135	1681	associated with the main app bundle
wenzelm@61135	1682
wenzelm@61135	1683	- isabelle jedit: settings
wenzelm@61135	1684	JEDIT_JAVA_SYSTEM_OPTIONS
wenzelm@61135	1685	JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64
wenzelm@61135	1686
wenzelm@61135	1687	- isabelle build: settings
wenzelm@61135	1688	ISABELLE_BUILD_JAVA_OPTIONS32 vs. ISABELLE_BUILD_JAVA_OPTIONS64
wenzelm@61135	1689
wenzelm@61294	1690	* Bash shell function "jvmpath" has been renamed to "platform_path": it
wenzelm@61294	1691	is relevant both for Poly/ML and JVM processes.
wenzelm@61294	1692
wenzelm@62017	1693	* Poly/ML default platform architecture may be changed from 32bit to
wenzelm@62205	1694	64bit via system option ML_system_64. A system restart (and rebuild) is
wenzelm@62205	1695	required after change.
wenzelm@62017	1696
wenzelm@62017	1697	* Poly/ML 5.6 runs natively on x86-windows and x86_64-windows, which
wenzelm@62017	1698	both allow larger heap space than former x86-cygwin.
wenzelm@62017	1699
wenzelm@62157	1700	* Heap images are 10-15% smaller due to less wasteful persistent theory
wenzelm@62157	1701	content (using ML type theory_id instead of theory);
wenzelm@62157	1702
wenzelm@60983	1703
wenzelm@60479	1704
wenzelm@60009	1705	New in Isabelle2015 (May 2015)
wenzelm@60009	1706	------------------------------
wenzelm@57695	1707
wenzelm@57941	1708	* General *
wenzelm@57941	1709
wenzelm@59939	1710	* Local theory specification commands may have a 'private' or
wenzelm@59990	1711	'qualified' modifier to restrict name space accesses to the local scope,
wenzelm@59939	1712	as provided by some "context begin ... end" block. For example:
wenzelm@59926	1713
wenzelm@59926	1714	context
wenzelm@59926	1715	begin
wenzelm@59926	1716
wenzelm@59926	1717	private definition ...
wenzelm@59926	1718	private lemma ...
wenzelm@59926	1719
wenzelm@59990	1720	qualified definition ...
wenzelm@59990	1721	qualified lemma ...
wenzelm@59990	1722
wenzelm@59926	1723	lemma ...
wenzelm@59926	1724	theorem ...
wenzelm@59926	1725
wenzelm@59926	1726	end
wenzelm@59926	1727
wenzelm@59901	1728	* Command 'experiment' opens an anonymous locale context with private
wenzelm@59901	1729	naming policy.
wenzelm@59901	1730
wenzelm@59951	1731	* Command 'notepad' requires proper nesting of begin/end and its proof
wenzelm@59951	1732	structure in the body: 'oops' is no longer supported here. Minor
wenzelm@59951	1733	INCOMPATIBILITY, use 'sorry' instead.
wenzelm@59951	1734
wenzelm@59951	1735	* Command 'named_theorems' declares a dynamic fact within the context,
wenzelm@59951	1736	together with an attribute to maintain the content incrementally. This
wenzelm@59951	1737	supersedes functor Named_Thms in Isabelle/ML, but with a subtle change
wenzelm@59951	1738	of semantics due to external visual order vs. internal reverse order.
wenzelm@59951	1739
wenzelm@59951	1740	* 'find_theorems': search patterns which are abstractions are
wenzelm@59951	1741	schematically expanded before search. Search results match the naive
wenzelm@59951	1742	expectation more closely, particularly wrt. abbreviations.
wenzelm@59951	1743	INCOMPATIBILITY.
wenzelm@59648	1744
wenzelm@59569	1745	* Commands 'method_setup' and 'attribute_setup' now work within a local
wenzelm@59569	1746	theory context.
wenzelm@57941	1747
wenzelm@58928	1748	* Outer syntax commands are managed authentically within the theory
wenzelm@59569	1749	context, without implicit global state. Potential for accidental
wenzelm@58928	1750	INCOMPATIBILITY, make sure that required theories are really imported.
wenzelm@58928	1751
wenzelm@60115	1752	* Historical command-line terminator ";" is no longer accepted (and
wenzelm@60115	1753	already used differently in Isar). Minor INCOMPATIBILITY, use "isabelle
wenzelm@60115	1754	update_semicolons" to remove obsolete semicolons from old theory
wenzelm@60115	1755	sources.
wenzelm@60115	1756
wenzelm@59951	1757	* Structural composition of proof methods (meth1; meth2) in Isar
wenzelm@59951	1758	corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
haftmann@59105	1759
wenzelm@60119	1760	* The Eisbach proof method language allows to define new proof methods
wenzelm@60119	1761	by combining existing ones with their usual syntax. The "match" proof
wenzelm@60119	1762	method provides basic fact/term matching in addition to
wenzelm@60119	1763	premise/conclusion matching through Subgoal.focus, and binds fact names
wenzelm@60288	1764	from matches as well as term patterns within matches. The Isabelle
wenzelm@60288	1765	documentation provides an entry "eisbach" for the Eisbach User Manual.
wenzelm@60288	1766	Sources and various examples are in ~~/src/HOL/Eisbach/.
wenzelm@60119	1767
wenzelm@57941	1768
wenzelm@58524	1769	* Prover IDE -- Isabelle/Scala/jEdit *
wenzelm@58524	1770
wenzelm@59569	1771	* Improved folding mode "isabelle" based on Isar syntax. Alternatively,
wenzelm@59569	1772	the "sidekick" mode may be used for document structure.
wenzelm@59569	1773
wenzelm@59569	1774	* Extended bracket matching based on Isar language structure. System
wenzelm@59569	1775	option jedit_structure_limit determines maximum number of lines to scan
wenzelm@59569	1776	in the buffer.
wenzelm@58758	1777
wenzelm@58540	1778	* Support for BibTeX files: context menu, context-sensitive token
wenzelm@58540	1779	marker, SideKick parser.
wenzelm@58524	1780
wenzelm@58551	1781	* Document antiquotation @{cite} provides formal markup, which is
wenzelm@60265	1782	interpreted semi-formally based on .bib files that happen to be open in
wenzelm@60265	1783	the editor (hyperlinks, completion etc.).
wenzelm@58551	1784
wenzelm@58785	1785	* Less waste of vertical space via negative line spacing (see Global
wenzelm@58785	1786	Options / Text Area).
wenzelm@58785	1787
wenzelm@60089	1788	* Improved graphview panel with optional output of PNG or PDF, for
wenzelm@60273	1789	display of 'thy_deps', 'class_deps' etc.
wenzelm@60009	1790
wenzelm@60115	1791	* The commands 'thy_deps' and 'class_deps' allow optional bounds to
wenzelm@60115	1792	restrict the visualized hierarchy.
wenzelm@60093	1793
wenzelm@60072	1794	* Improved scheduling for asynchronous print commands (e.g. provers
wenzelm@60072	1795	managed by the Sledgehammer panel) wrt. ongoing document processing.
wenzelm@60072	1796
wenzelm@58524	1797
wenzelm@59951	1798	* Document preparation *
wenzelm@59951	1799
wenzelm@59951	1800	* Document markup commands 'chapter', 'section', 'subsection',
wenzelm@59951	1801	'subsubsection', 'text', 'txt', 'text_raw' work uniformly in any
wenzelm@59951	1802	context, even before the initial 'theory' command. Obsolete proof
wenzelm@59951	1803	commands 'sect', 'subsect', 'subsubsect', 'txt_raw' have been
wenzelm@59951	1804	discontinued, use 'section', 'subsection', 'subsubsection', 'text_raw'
wenzelm@59951	1805	instead. The old 'header' command is still retained for some time, but
wenzelm@59951	1806	should be replaced by 'chapter', 'section' etc. (using "isabelle
wenzelm@59951	1807	update_header"). Minor INCOMPATIBILITY.
wenzelm@59951	1808
wenzelm@60009	1809	* Official support for "tt" style variants, via \isatt{...} or
wenzelm@60009	1810	\begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
wenzelm@60009	1811	verbatim environment of LaTeX is no longer used. This allows @{ML} etc.
wenzelm@60009	1812	as argument to other macros (such as footnotes).
wenzelm@60009	1813
wenzelm@60009	1814	* Document antiquotation @{verbatim} prints ASCII text literally in "tt"
wenzelm@60009	1815	style.
wenzelm@60009	1816
wenzelm@60009	1817	* Discontinued obsolete option "document_graph": session_graph.pdf is
wenzelm@60009	1818	produced unconditionally for HTML browser_info and PDF-LaTeX document.
wenzelm@60009	1819
wenzelm@59951	1820	* Diagnostic commands and document markup commands within a proof do not
wenzelm@59951	1821	affect the command tag for output. Thus commands like 'thm' are subject
wenzelm@59951	1822	to proof document structure, and no longer "stick out" accidentally.
wenzelm@59951	1823	Commands 'text' and 'txt' merely differ in the LaTeX style, not their
wenzelm@59951	1824	tags. Potential INCOMPATIBILITY in exotic situations.
wenzelm@59951	1825
wenzelm@59951	1826	* System option "pretty_margin" is superseded by "thy_output_margin",
wenzelm@59951	1827	which is also accessible via document antiquotation option "margin".
wenzelm@59951	1828	Only the margin for document output may be changed, but not the global
wenzelm@59951	1829	pretty printing: that is 76 for plain console output, and adapted
wenzelm@59951	1830	dynamically in GUI front-ends. Implementations of document
wenzelm@59951	1831	antiquotations need to observe the margin explicitly according to
wenzelm@59951	1832	Thy_Output.string_of_margin. Minor INCOMPATIBILITY.
wenzelm@59951	1833
wenzelm@60299	1834	* Specification of 'document_files' in the session ROOT file is
wenzelm@60299	1835	mandatory for document preparation. The legacy mode with implicit
wenzelm@60299	1836	copying of the document/ directory is no longer supported. Minor
wenzelm@60299	1837	INCOMPATIBILITY.
wenzelm@60299	1838
wenzelm@59951	1839
haftmann@58202	1840	* Pure *
haftmann@58202	1841
wenzelm@59835	1842	* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
wenzelm@59835	1843	etc.) allow an optional context of local variables ('for' declaration):
wenzelm@59835	1844	these variables become schematic in the instantiated theorem; this
wenzelm@59835	1845	behaviour is analogous to 'for' in attributes "where" and "of".
wenzelm@59835	1846	Configuration option rule_insts_schematic (default false) controls use
wenzelm@59835	1847	of schematic variables outside the context. Minor INCOMPATIBILITY,
wenzelm@59835	1848	declare rule_insts_schematic = true temporarily and update to use local
wenzelm@59835	1849	variable declarations or dummy patterns instead.
wenzelm@59835	1850
wenzelm@60009	1851	* Explicit instantiation via attributes "where", "of", and proof methods
wenzelm@60009	1852	"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
wenzelm@60009	1853	("_") that stand for anonymous local variables.
wenzelm@60009	1854
wenzelm@59951	1855	* Generated schematic variables in standard format of exported facts are
wenzelm@59951	1856	incremented to avoid material in the proof context. Rare
wenzelm@59951	1857	INCOMPATIBILITY, explicit instantiation sometimes needs to refer to
wenzelm@59951	1858	different index.
wenzelm@59951	1859
wenzelm@60010	1860	* Lexical separation of signed and unsigned numerals: categories "num"
wenzelm@60010	1861	and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
wenzelm@60010	1862	of numeral signs, particularly in expressions involving infix syntax
wenzelm@60010	1863	like "(- 1) ^ n".
haftmann@58410	1864
wenzelm@58421	1865	* Old inner token category "xnum" has been discontinued. Potential
wenzelm@58421	1866	INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
wenzelm@58421	1867	token category instead.
wenzelm@58421	1868
haftmann@58202	1869
blanchet@57737	1870	* HOL *
blanchet@57737	1871
blanchet@57983	1872	* New (co)datatype package:
blanchet@58373	1873	- The 'datatype_new' command has been renamed 'datatype'. The old
blanchet@58373	1874	command of that name is now called 'old_datatype' and is provided
blanchet@58373	1875	by "~~/src/HOL/Library/Old_Datatype.thy". See
blanchet@58373	1876	'isabelle doc datatypes' for information on porting.
blanchet@58373	1877	INCOMPATIBILITY.
blanchet@57983	1878	- Renamed theorems:
blanchet@57983	1879	disc_corec ~> corec_disc
blanchet@57983	1880	disc_corec_iff ~> corec_disc_iff
blanchet@57983	1881	disc_exclude ~> distinct_disc
blanchet@57983	1882	disc_exhaust ~> exhaust_disc
blanchet@57983	1883	disc_map_iff ~> map_disc_iff
blanchet@57983	1884	sel_corec ~> corec_sel
blanchet@57983	1885	sel_exhaust ~> exhaust_sel
blanchet@57983	1886	sel_map ~> map_sel
blanchet@57983	1887	sel_set ~> set_sel
blanchet@57983	1888	sel_split ~> split_sel
blanchet@57983	1889	sel_split_asm ~> split_sel_asm
blanchet@57983	1890	strong_coinduct ~> coinduct_strong
blanchet@57983	1891	weak_case_cong ~> case_cong_weak
blanchet@57983	1892	INCOMPATIBILITY.
blanchet@58192	1893	- The "no_code" option to "free_constructors", "datatype_new", and
blanchet@58192	1894	"codatatype" has been renamed "plugins del: code".
blanchet@58192	1895	INCOMPATIBILITY.
blanchet@58044	1896	- The rules "set_empty" have been removed. They are easy
blanchet@58044	1897	consequences of other set rules "by auto".
blanchet@58044	1898	INCOMPATIBILITY.
blanchet@58044	1899	- The rule "set_cases" is now registered with the "[cases set]"
blanchet@57990	1900	attribute. This can influence the behavior of the "cases" proof
blanchet@57990	1901	method when more than one case rule is applicable (e.g., an
blanchet@57990	1902	assumption is of the form "w : set ws" and the method "cases w"
blanchet@57990	1903	is invoked). The solution is to specify the case rule explicitly
blanchet@57990	1904	(e.g. "cases w rule: widget.exhaust").
blanchet@57990	1905	INCOMPATIBILITY.
blanchet@59675	1906	- Renamed theories:
blanchet@59675	1907	BNF_Comp ~> BNF_Composition
blanchet@59675	1908	BNF_FP_Base ~> BNF_Fixpoint_Base
blanchet@59675	1909	BNF_GFP ~> BNF_Greatest_Fixpoint
blanchet@59675	1910	BNF_LFP ~> BNF_Least_Fixpoint
blanchet@59675	1911	BNF_Constructions_on_Wellorders ~> BNF_Wellorder_Constructions
blanchet@59675	1912	Cardinals/Constructions_on_Wellorders ~> Cardinals/Wellorder_Constructions
blanchet@59675	1913	INCOMPATIBILITY.
wenzelm@60114	1914	- Lifting and Transfer setup for basic HOL types sum and prod (also
wenzelm@60114	1915	option) is now performed by the BNF package. Theories Lifting_Sum,
wenzelm@60114	1916	Lifting_Product and Lifting_Option from Main became obsolete and
wenzelm@60114	1917	were removed. Changed definitions of the relators rel_prod and
wenzelm@60114	1918	rel_sum (using inductive).
traytel@60111	1919	INCOMPATIBILITY: use rel_prod.simps and rel_sum.simps instead
wenzelm@60114	1920	of rel_prod_def and rel_sum_def.
wenzelm@60114	1921	Minor INCOMPATIBILITY: (rarely used by name) transfer theorem names
wenzelm@60114	1922	changed (e.g. map_prod_transfer ~> prod.map_transfer).
wenzelm@60261	1923	- Parametricity theorems for map functions, relators, set functions,
wenzelm@60261	1924	constructors, case combinators, discriminators, selectors and
wenzelm@60261	1925	(co)recursors are automatically proved and registered as transfer
wenzelm@60261	1926	rules.
blanchet@57983	1927
blanchet@57983	1928	* Old datatype package:
blanchet@58310	1929	- The old 'datatype' command has been renamed 'old_datatype', and
blanchet@58373	1930	'rep_datatype' has been renamed 'old_rep_datatype'. They are
blanchet@58373	1931	provided by "~~/src/HOL/Library/Old_Datatype.thy". See
blanchet@58310	1932	'isabelle doc datatypes' for information on porting.
blanchet@58373	1933	INCOMPATIBILITY.
blanchet@57983	1934	- Renamed theorems:
blanchet@57983	1935	weak_case_cong ~> case_cong_weak
blanchet@57983	1936	INCOMPATIBILITY.
blanchet@58373	1937	- Renamed theory:
blanchet@58373	1938	~~/src/HOL/Datatype.thy ~> ~~/src/HOL/Library/Old_Datatype.thy
blanchet@58373	1939	INCOMPATIBILITY.
blanchet@57983	1940
blanchet@59039	1941	* Nitpick:
wenzelm@60010	1942	- Fixed soundness bug related to the strict and non-strict subset
blanchet@59039	1943	operations.
blanchet@59039	1944
blanchet@57737	1945	* Sledgehammer:
blanchet@59511	1946	- CVC4 is now included with Isabelle instead of CVC3 and run by
blanchet@59511	1947	default.
blanchet@59965	1948	- Z3 is now always enabled by default, now that it is fully open
blanchet@59965	1949	source. The "z3_non_commercial" option is discontinued.
blanchet@57737	1950	- Minimization is now always enabled by default.
wenzelm@60010	1951	Removed sub-command:
blanchet@57737	1952	min
blanchet@59967	1953	- Proof reconstruction, both one-liners and Isar, has been
blanchet@59039	1954	dramatically improved.
blanchet@59039	1955	- Improved support for CVC4 and veriT.
blanchet@57737	1956
blanchet@58062	1957	* Old and new SMT modules:
blanchet@58067	1958	- The old 'smt' method has been renamed 'old_smt' and moved to
wenzelm@59569	1959	'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,
wenzelm@59569	1960	until applications have been ported to use the new 'smt' method. For
wenzelm@59569	1961	the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must
wenzelm@59569	1962	be installed, and the environment variable "OLD_Z3_SOLVER" must
wenzelm@59569	1963	point to it.
blanchet@58062	1964	INCOMPATIBILITY.
blanchet@58067	1965	- The 'smt2' method has been renamed 'smt'.
blanchet@58060	1966	INCOMPATIBILITY.
wenzelm@59569	1967	- New option 'smt_reconstruction_step_timeout' to limit the
wenzelm@59569	1968	reconstruction time of Z3 proof steps in the new 'smt' method.
boehmes@59216	1969	- New option 'smt_statistics' to display statistics of the new 'smt'
boehmes@59216	1970	method, especially runtime statistics of Z3 proof reconstruction.
blanchet@58060	1971
wenzelm@60261	1972	* Lifting: command 'lift_definition' allows to execute lifted constants
wenzelm@60261	1973	that have as a return type a datatype containing a subtype. This
wenzelm@60261	1974	overcomes long-time limitations in the area of code generation and
wenzelm@60261	1975	lifting, and avoids tedious workarounds.
kuncar@60258	1976
wenzelm@60009	1977	* Command and antiquotation "value" provide different evaluation slots
wenzelm@60009	1978	(again), where the previous strategy (NBE after ML) serves as default.
wenzelm@60009	1979	Minor INCOMPATIBILITY.
wenzelm@60009	1980
wenzelm@60009	1981	* Add NO_MATCH-simproc, allows to check for syntactic non-equality.
wenzelm@60009	1982
wenzelm@60009	1983	* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
wenzelm@60009	1984	non-termination in case of distributing a division. With this change
wenzelm@60009	1985	field_simps is in some cases slightly less powerful, if it fails try to
wenzelm@60009	1986	add algebra_simps, or use divide_simps. Minor INCOMPATIBILITY.
wenzelm@60009	1987
wenzelm@60009	1988	* Separate class no_zero_divisors has been given up in favour of fully
wenzelm@60009	1989	algebraic semiring_no_zero_divisors. INCOMPATIBILITY.
wenzelm@60009	1990
wenzelm@60009	1991	* Class linordered_semidom really requires no zero divisors.
wenzelm@60009	1992	INCOMPATIBILITY.
wenzelm@60009	1993
wenzelm@60009	1994	* Classes division_ring, field and linordered_field always demand
wenzelm@60009	1995	"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
wenzelm@60009	1996	field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
wenzelm@60009	1997
wenzelm@60009	1998	* Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
wenzelm@60009	1999	additive inverse operation. INCOMPATIBILITY.
wenzelm@60009	2000
lp15@60020	2001	* Complex powers and square roots. The functions "ln" and "powr" are now
wenzelm@60025	2002	overloaded for types real and complex, and 0 powr y = 0 by definition.
wenzelm@60025	2003	INCOMPATIBILITY: type constraints may be necessary.
lp15@60020	2004
wenzelm@60009	2005	* The functions "sin" and "cos" are now defined for any type of sort
wenzelm@60009	2006	"{real_normed_algebra_1,banach}" type, so in particular on "real" and
wenzelm@60009	2007	"complex" uniformly. Minor INCOMPATIBILITY: type constraints may be
wenzelm@60009	2008	needed.
wenzelm@60009	2009
wenzelm@60009	2010	* New library of properties of the complex transcendental functions sin,
wenzelm@60009	2011	cos, tan, exp, Ln, Arctan, Arcsin, Arccos. Ported from HOL Light.
wenzelm@60009	2012
wenzelm@60009	2013	* The factorial function, "fact", now has type "nat => 'a" (of a sort
wenzelm@60009	2014	that admits numeric types including nat, int, real and complex.
wenzelm@60009	2015	INCOMPATIBILITY: an expression such as "fact 3 = 6" may require a type
wenzelm@60009	2016	constraint, and the combination "real (fact k)" is likely to be
wenzelm@60009	2017	unsatisfactory. If a type conversion is still necessary, then use
wenzelm@60009	2018	"of_nat (fact k)" or "real_of_nat (fact k)".
wenzelm@60009	2019
wenzelm@60009	2020	* Removed functions "natfloor" and "natceiling", use "nat o floor" and
wenzelm@60009	2021	"nat o ceiling" instead. A few of the lemmas have been retained and
wenzelm@60009	2022	adapted: in their names "natfloor"/"natceiling" has been replaced by
wenzelm@60009	2023	"nat_floor"/"nat_ceiling".
wenzelm@60009	2024
wenzelm@60009	2025	* Qualified some duplicated fact names required for boostrapping the
wenzelm@60009	2026	type class hierarchy:
wenzelm@60009	2027	ab_add_uminus_conv_diff ~> diff_conv_add_uminus
wenzelm@60009	2028	field_inverse_zero ~> inverse_zero
wenzelm@60009	2029	field_divide_inverse ~> divide_inverse
wenzelm@60009	2030	field_inverse ~> left_inverse
wenzelm@60009	2031	Minor INCOMPATIBILITY.
wenzelm@60009	2032
wenzelm@60009	2033	* Eliminated fact duplicates:
wenzelm@60009	2034	mult_less_imp_less_right ~> mult_right_less_imp_less
wenzelm@60009	2035	mult_less_imp_less_left ~> mult_left_less_imp_less
wenzelm@60009	2036	Minor INCOMPATIBILITY.
wenzelm@60009	2037
wenzelm@60009	2038	* Fact consolidation: even_less_0_iff is subsumed by
wenzelm@60009	2039	double_add_less_zero_iff_single_add_less_zero (simp by default anyway).
wenzelm@60009	2040
wenzelm@60009	2041	* Generalized and consolidated some theorems concerning divsibility:
wenzelm@60009	2042	dvd_reduce ~> dvd_add_triv_right_iff
wenzelm@60009	2043	dvd_plus_eq_right ~> dvd_add_right_iff
wenzelm@60009	2044	dvd_plus_eq_left ~> dvd_add_left_iff
wenzelm@60009	2045	Minor INCOMPATIBILITY.
wenzelm@60009	2046
wenzelm@60009	2047	* "even" and "odd" are mere abbreviations for "2 dvd _" and "~ 2 dvd _"
wenzelm@60009	2048	and part of theory Main.
wenzelm@60009	2049	even_def ~> even_iff_mod_2_eq_zero
wenzelm@60009	2050	INCOMPATIBILITY.
wenzelm@60009	2051
wenzelm@60009	2052	* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1. Minor
wenzelm@60009	2053	INCOMPATIBILITY.
wenzelm@60009	2054
wenzelm@60009	2055	* Bootstrap of listsum as special case of abstract product over lists.
wenzelm@60009	2056	Fact rename:
wenzelm@60009	2057	listsum_def ~> listsum.eq_foldr
wenzelm@60009	2058	INCOMPATIBILITY.
wenzelm@60009	2059
wenzelm@60009	2060	* Product over lists via constant "listprod".
wenzelm@60009	2061
wenzelm@60009	2062	* Theory List: renamed drop_Suc_conv_tl and nth_drop' to
wenzelm@60009	2063	Cons_nth_drop_Suc.
nipkow@58247	2064
Andreas@58626	2065	* New infrastructure for compiling, running, evaluating and testing
wenzelm@59569	2066	generated code in target languages in HOL/Library/Code_Test. See
wenzelm@59569	2067	HOL/Codegenerator_Test/Code_Test* for examples.
wenzelm@58008	2068
wenzelm@60009	2069	* Library/Multiset:
blanchet@59813	2070	- Introduced "replicate_mset" operation.
blanchet@59813	2071	- Introduced alternative characterizations of the multiset ordering in
blanchet@59813	2072	"Library/Multiset_Order".
blanchet@59958	2073	- Renamed multiset ordering:
blanchet@59958	2074	<# ~> #<#
blanchet@59958	2075	<=# ~> #<=#
blanchet@59958	2076	\<subset># ~> #\<subset>#
blanchet@59958	2077	\<subseteq># ~> #\<subseteq>#
blanchet@59958	2078	INCOMPATIBILITY.
blanchet@59986	2079	- Introduced abbreviations for ill-named multiset operations:
blanchet@59986	2080	<#, \<subset># abbreviate < (strict subset)
blanchet@59986	2081	<=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
blanchet@59986	2082	INCOMPATIBILITY.
blanchet@59813	2083	- Renamed
blanchet@59813	2084	in_multiset_of ~> in_multiset_in_set
nipkow@59998	2085	Multiset.fold ~> fold_mset
nipkow@59998	2086	Multiset.filter ~> filter_mset
blanchet@59813	2087	INCOMPATIBILITY.
nipkow@59949	2088	- Removed mcard, is equal to size.
blanchet@59813	2089	- Added attributes:
blanchet@59813	2090	image_mset.id [simp]
blanchet@59813	2091	image_mset_id [simp]
blanchet@59813	2092	elem_multiset_of_set [simp, intro]
blanchet@59813	2093	comp_fun_commute_plus_mset [simp]
blanchet@59813	2094	comp_fun_commute.fold_mset_insert [OF comp_fun_commute_plus_mset, simp]
blanchet@59813	2095	in_mset_fold_plus_iff [iff]
blanchet@59813	2096	set_of_Union_mset [simp]
blanchet@59813	2097	in_Union_mset_iff [iff]
blanchet@59813	2098	INCOMPATIBILITY.
blanchet@59813	2099
wenzelm@60009	2100	* Library/Sum_of_Squares: simplified and improved "sos" method. Always
wenzelm@60009	2101	use local CSDP executable, which is much faster than the NEOS server.
wenzelm@60009	2102	The "sos_cert" functionality is invoked as "sos" with additional
wenzelm@60009	2103	argument. Minor INCOMPATIBILITY.
wenzelm@60009	2104
wenzelm@60009	2105	* HOL-Decision_Procs: New counterexample generator quickcheck
wenzelm@60009	2106	[approximation] for inequalities of transcendental functions. Uses
wenzelm@60009	2107	hardware floating point arithmetic to randomly discover potential
wenzelm@60010	2108	counterexamples. Counterexamples are certified with the "approximation"
wenzelm@60009	2109	method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
wenzelm@60009	2110	examples.
immler@58990	2111
hoelzl@59354	2112	* HOL-Probability: Reworked measurability prover
wenzelm@60010	2113	- applies destructor rules repeatedly
hoelzl@59354	2114	- removed application splitting (replaced by destructor rule)
wenzelm@59569	2115	- added congruence rules to rewrite measure spaces under the sets
wenzelm@59569	2116	projection
wenzelm@59569	2117
wenzelm@60009	2118	* New proof method "rewrite" (in theory ~~/src/HOL/Library/Rewrite) for
wenzelm@60009	2119	single-step rewriting with subterm selection based on patterns.
wenzelm@60009	2120
wenzelm@58630	2121
blanchet@58066	2122	* ML *
blanchet@58066	2123
wenzelm@60009	2124	* Subtle change of name space policy: undeclared entries are now
wenzelm@60009	2125	considered inaccessible, instead of accessible via the fully-qualified
wenzelm@60009	2126	internal name. This mainly affects Name_Space.intern (and derivatives),
wenzelm@60009	2127	which may produce an unexpected Long_Name.hidden prefix. Note that
wenzelm@60010	2128	contemporary applications use the strict Name_Space.check (and
wenzelm@60009	2129	derivatives) instead, which is not affected by the change. Potential
wenzelm@60009	2130	INCOMPATIBILITY in rare applications of Name_Space.intern.
wenzelm@59951	2131
wenzelm@60094	2132	* Subtle change of error semantics of Toplevel.proof_of: regular user
wenzelm@60094	2133	ERROR instead of internal Toplevel.UNDEF.
wenzelm@60094	2134
wenzelm@59951	2135	* Basic combinators map, fold, fold_map, split_list, apply are available
wenzelm@59951	2136	as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
wenzelm@59951	2137
wenzelm@59951	2138	* Renamed "pairself" to "apply2", in accordance to @{apply 2}.
wenzelm@59951	2139	INCOMPATIBILITY.
wenzelm@59951	2140
wenzelm@59951	2141	* Former combinators NAMED_CRITICAL and CRITICAL for central critical
wenzelm@59951	2142	sections have been discontinued, in favour of the more elementary
wenzelm@59951	2143	Multithreading.synchronized and its high-level derivative
wenzelm@59951	2144	Synchronized.var (which is usually sufficient in applications). Subtle
wenzelm@59951	2145	INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
wenzelm@59951	2146	nested.
wenzelm@59951	2147
wenzelm@60009	2148	* Synchronized.value (ML) is actually synchronized (as in Scala): subtle
wenzelm@60009	2149	change of semantics with minimal potential for INCOMPATIBILITY.
wenzelm@59899	2150
wenzelm@59621	2151	* The main operations to certify logical entities are Thm.ctyp_of and
wenzelm@59621	2152	Thm.cterm_of with a local context; old-style global theory variants are
wenzelm@59621	2153	available as Thm.global_ctyp_of and Thm.global_cterm_of.
wenzelm@59621	2154	INCOMPATIBILITY.
wenzelm@59621	2155
wenzelm@59582	2156	* Elementary operations in module Thm are no longer pervasive.
wenzelm@59582	2157	INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of,
wenzelm@59582	2158	Thm.term_of etc.
wenzelm@59582	2159
wenzelm@58963	2160	* Proper context for various elementary tactics: assume_tac,
wenzelm@59498	2161	resolve_tac, eresolve_tac, dresolve_tac, forward_tac, match_tac,
wenzelm@59498	2162	compose_tac, Splitter.split_tac etc. INCOMPATIBILITY.
wenzelm@58956	2163
blanchet@58066	2164	* Tactical PARALLEL_ALLGOALS is the most common way to refer to
blanchet@58066	2165	PARALLEL_GOALS.
blanchet@58066	2166
wenzelm@59564	2167	* Goal.prove_multi is superseded by the fully general Goal.prove_common,
wenzelm@59564	2168	which also allows to specify a fork priority.
wenzelm@59564	2169
wenzelm@59936	2170	* Antiquotation @{command_spec "COMMAND"} is superseded by
wenzelm@59936	2171	@{command_keyword COMMAND} (usually without quotes and with PIDE
wenzelm@59936	2172	markup). Minor INCOMPATIBILITY.
wenzelm@59936	2173
wenzelm@60009	2174	* Cartouches within ML sources are turned into values of type
wenzelm@60009	2175	Input.source (with formal position information).
wenzelm@60009	2176
blanchet@58066	2177
wenzelm@58610	2178	* System *
wenzelm@58610	2179
wenzelm@59951	2180	* The Isabelle tool "update_cartouches" changes theory files to use
wenzelm@59951	2181	cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
wenzelm@59951	2182
wenzelm@60106	2183	* The Isabelle tool "build" provides new options -X, -k, -x.
wenzelm@59951	2184
wenzelm@59951	2185	* Discontinued old-fashioned "codegen" tool. Code generation can always
wenzelm@59951	2186	be externally triggered using an appropriate ROOT file plus a
wenzelm@59951	2187	corresponding theory. Parametrization is possible using environment
wenzelm@59951	2188	variables, or ML snippets in the most extreme cases. Minor
wenzelm@59951	2189	INCOMPATIBILITY.
wenzelm@58842	2190
wenzelm@59200	2191	* JVM system property "isabelle.threads" determines size of Scala thread
wenzelm@59200	2192	pool, like Isabelle system option "threads" for ML.
wenzelm@59200	2193
wenzelm@59201	2194	* JVM system property "isabelle.laf" determines the default Swing
wenzelm@59201	2195	look-and-feel, via internal class name or symbolic name as in the jEdit
wenzelm@59201	2196	menu Global Options / Appearance.
wenzelm@59201	2197
wenzelm@59951	2198	* Support for Proof General and Isar TTY loop has been discontinued.
wenzelm@60009	2199	Minor INCOMPATIBILITY, use standard PIDE infrastructure instead.
wenzelm@59891	2200
wenzelm@58610	2201
wenzelm@57695	2202
wenzelm@57452	2203	New in Isabelle2014 (August 2014)
wenzelm@57452	2204	---------------------------------
wenzelm@54055	2205
wenzelm@54702	2206	* General *
wenzelm@54702	2207
wenzelm@57452	2208	* Support for official Standard ML within the Isabelle context.
wenzelm@57452	2209	Command 'SML_file' reads and evaluates the given Standard ML file.
wenzelm@57452	2210	Toplevel bindings are stored within the theory context; the initial
wenzelm@57452	2211	environment is restricted to the Standard ML implementation of
wenzelm@57452	2212	Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import'
wenzelm@57452	2213	and 'SML_export' allow to exchange toplevel bindings between the two
wenzelm@57452	2214	separate environments. See also ~~/src/Tools/SML/Examples.thy for
wenzelm@57452	2215	some examples.
wenzelm@56499	2216
wenzelm@57504	2217	* Standard tactics and proof methods such as "clarsimp", "auto" and
wenzelm@57504	2218	"safe" now preserve equality hypotheses "x = expr" where x is a free
wenzelm@57504	2219	variable. Locale assumptions and chained facts containing "x"
wenzelm@57504	2220	continue to be useful. The new method "hypsubst_thin" and the
wenzelm@57504	2221	configuration option "hypsubst_thin" (within the attribute name space)
wenzelm@57504	2222	restore the previous behavior. INCOMPATIBILITY, especially where
wenzelm@57504	2223	induction is done after these methods or when the names of free and
wenzelm@57504	2224	bound variables clash. As first approximation, old proofs may be
wenzelm@57504	2225	repaired by "using [[hypsubst_thin = true]]" in the critical spot.
wenzelm@57504	2226
wenzelm@56232	2227	* More static checking of proof methods, which allows the system to
wenzelm@56232	2228	form a closure over the concrete syntax. Method arguments should be
wenzelm@56232	2229	processed in the original proof context as far as possible, before
wenzelm@56232	2230	operating on the goal state. In any case, the standard discipline for
wenzelm@56232	2231	subgoal-addressing needs to be observed: no subgoals or a subgoal
wenzelm@56232	2232	number that is out of range produces an empty result sequence, not an
wenzelm@56232	2233	exception. Potential INCOMPATIBILITY for non-conformant tactical
wenzelm@56232	2234	proof tools.
wenzelm@56232	2235
wenzelm@57452	2236	* Lexical syntax (inner and outer) supports text cartouches with
wenzelm@57452	2237	arbitrary nesting, and without escapes of quotes etc. The Prover IDE
wenzelm@57452	2238	supports input via ` (backquote).
wenzelm@57452	2239
wenzelm@57452	2240	* The outer syntax categories "text" (for formal comments and document
wenzelm@57452	2241	markup commands) and "altstring" (for literal fact references) allow
wenzelm@57452	2242	cartouches as well, in addition to the traditional mix of quotations.
wenzelm@57452	2243
wenzelm@57452	2244	* Syntax of document antiquotation @{rail} now uses \<newline> instead
wenzelm@57452	2245	of "\\", to avoid the optical illusion of escaped backslash within
wenzelm@57491	2246	string token. General renovation of its syntax using text cartouches.
wenzelm@57452	2247	Minor INCOMPATIBILITY.
wenzelm@57452	2248
wenzelm@57452	2249	* Discontinued legacy_isub_isup, which was a temporary workaround for
wenzelm@57452	2250	Isabelle/ML in Isabelle2013-1. The prover process no longer accepts
wenzelm@57452	2251	old identifier syntax with \<^isub> or \<^isup>. Potential
wenzelm@57452	2252	INCOMPATIBILITY.
wenzelm@57452	2253
wenzelm@57452	2254	* Document antiquotation @{url} produces markup for the given URL,
wenzelm@57452	2255	which results in an active hyperlink within the text.
wenzelm@57452	2256
wenzelm@57452	2257	* Document antiquotation @{file_unchecked} is like @{file}, but does
wenzelm@57452	2258	not check existence within the file-system.
wenzelm@57452	2259
wenzelm@57452	2260	* Updated and extended manuals: codegen, datatypes, implementation,
wenzelm@57452	2261	isar-ref, jedit, system.
wenzelm@57423	2262
wenzelm@54702	2263
wenzelm@54533	2264	* Prover IDE -- Isabelle/Scala/jEdit *
wenzelm@54533	2265
wenzelm@57650	2266	* Improved Document panel: simplified interaction where every single
wenzelm@57452	2267	mouse click (re)opens document via desktop environment or as jEdit
wenzelm@57452	2268	buffer.
wenzelm@57452	2269
wenzelm@57452	2270	* Support for Navigator plugin (with toolbar buttons), with connection
wenzelm@57452	2271	to PIDE hyperlinks.
wenzelm@57452	2272
wenzelm@57452	2273	* Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
wenzelm@57452	2274	Open text buffers take precedence over copies within the file-system.
wenzelm@57452	2275
wenzelm@57452	2276	* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
wenzelm@57452	2277	auxiliary ML files.
wenzelm@57423	2278
wenzelm@57423	2279	* Improved syntactic and semantic completion mechanism, with simple
wenzelm@57423	2280	templates, completion language context, name-space completion,
wenzelm@57423	2281	file-name completion, spell-checker completion.
wenzelm@57423	2282
wenzelm@57423	2283	* Refined GUI popup for completion: more robust key/mouse event
wenzelm@57423	2284	handling and propagation to enclosing text area -- avoid loosing
wenzelm@57423	2285	keystrokes with slow / remote graphics displays.
wenzelm@57423	2286
wenzelm@57833	2287	* Completion popup supports both ENTER and TAB (default) to select an
wenzelm@57833	2288	item, depending on Isabelle options.
wenzelm@57833	2289
wenzelm@57423	2290	* Refined insertion of completion items wrt. jEdit text: multiple
wenzelm@57423	2291	selections, rectangular selections, rectangular selection as "tall
wenzelm@57423	2292	caret".
wenzelm@56342	2293
wenzelm@56580	2294	* Integrated spell-checker for document text, comments etc. with
wenzelm@57423	2295	completion popup and context-menu.
wenzelm@56554	2296
wenzelm@56879	2297	* More general "Query" panel supersedes "Find" panel, with GUI access
wenzelm@56879	2298	to commands 'find_theorems' and 'find_consts', as well as print
wenzelm@56879	2299	operations for the context. Minor incompatibility in keyboard
wenzelm@56879	2300	shortcuts etc.: replace action isabelle-find by isabelle-query.
wenzelm@56761	2301
wenzelm@56901	2302	* Search field for all output panels ("Output", "Query", "Info" etc.)
wenzelm@56901	2303	to highlight text via regular expression.
wenzelm@56901	2304
wenzelm@54881	2305	* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
wenzelm@54881	2306	General") allows to specify additional print modes for the prover
wenzelm@54881	2307	process, without requiring old-fashioned command-line invocation of
wenzelm@54881	2308	"isabelle jedit -m MODE".
wenzelm@54881	2309
wenzelm@56505	2310	* More support for remote files (e.g. http) using standard Java
wenzelm@56505	2311	networking operations instead of jEdit virtual file-systems.
wenzelm@56505	2312
wenzelm@57822	2313	* Empty editors buffers that are no longer required (e.g.\ via theory
wenzelm@57822	2314	imports) are automatically removed from the document model.
wenzelm@57822	2315
wenzelm@57869	2316	* Improved monitor panel.
wenzelm@57869	2317
wenzelm@56838	2318	* Improved Console/Scala plugin: more uniform scala.Console output,
wenzelm@56838	2319	more robust treatment of threads and interrupts.
wenzelm@56838	2320
wenzelm@56939	2321	* Improved management of dockable windows: clarified keyboard focus
wenzelm@56939	2322	and window placement wrt. main editor view; optional menu item to
wenzelm@56939	2323	"Detach" a copy where this makes sense.
wenzelm@56939	2324
wenzelm@57452	2325	* New Simplifier Trace panel provides an interactive view of the
wenzelm@57591	2326	simplification process, enabled by the "simp_trace_new" attribute
wenzelm@57452	2327	within the context.
wenzelm@57452	2328
wenzelm@57452	2329
wenzelm@55001	2330	* Pure *
wenzelm@55001	2331
wenzelm@57504	2332	* Low-level type-class commands 'classes', 'classrel', 'arities' have
wenzelm@57504	2333	been discontinued to avoid the danger of non-trivial axiomatization
wenzelm@57504	2334	that is not immediately visible. INCOMPATIBILITY, use regular
wenzelm@57504	2335	'instance' command with proof. The required OFCLASS(...) theorem
wenzelm@57504	2336	might be postulated via 'axiomatization' beforehand, or the proof
wenzelm@57504	2337	finished trivially if the underlying class definition is made vacuous
wenzelm@57504	2338	(without any assumptions). See also Isabelle/ML operations
wenzelm@57504	2339	Axclass.class_axiomatization, Axclass.classrel_axiomatization,
wenzelm@57504	2340	Axclass.arity_axiomatization.
wenzelm@57504	2341
wenzelm@56245	2342	* Basic constants of Pure use more conventional names and are always
wenzelm@56245	2343	qualified. Rare INCOMPATIBILITY, but with potentially serious
wenzelm@56245	2344	consequences, notably for tools in Isabelle/ML. The following
wenzelm@56245	2345	renaming needs to be applied:
wenzelm@56245	2346
wenzelm@56245	2347	== ~> Pure.eq
wenzelm@56245	2348	==> ~> Pure.imp
wenzelm@56245	2349	all ~> Pure.all
wenzelm@56245	2350	TYPE ~> Pure.type
wenzelm@56245	2351	dummy_pattern ~> Pure.dummy_pattern
wenzelm@56245	2352
wenzelm@56245	2353	Systematic porting works by using the following theory setup on a
wenzelm@56245	2354	previous Isabelle version to introduce the new name accesses for the
wenzelm@56245	2355	old constants:
wenzelm@56245	2356
wenzelm@56245	2357	setup {*
wenzelm@56245	2358	fn thy => thy
wenzelm@56245	2359	\|> Sign.root_path
wenzelm@56245	2360	\|> Sign.const_alias (Binding.qualify true "Pure" @{binding eq}) "=="
wenzelm@56245	2361	\|> Sign.const_alias (Binding.qualify true "Pure" @{binding imp}) "==>"
wenzelm@56245	2362	\|> Sign.const_alias (Binding.qualify true "Pure" @{binding all}) "all"
wenzelm@56245	2363	\|> Sign.restore_naming thy
wenzelm@56245	2364	*}
wenzelm@56245	2365
wenzelm@56245	2366	Thus ML antiquotations like @{const_name Pure.eq} may be used already.
wenzelm@56245	2367	Later the application is moved to the current Isabelle version, and
wenzelm@56245	2368	the auxiliary aliases are deleted.
wenzelm@56245	2369
wenzelm@55143	2370	* Attributes "where" and "of" allow an optional context of local
wenzelm@55143	2371	variables ('for' declaration): these variables become schematic in the
wenzelm@55143	2372	instantiated theorem.
wenzelm@55143	2373
wenzelm@55152	2374	* Obsolete attribute "standard" has been discontinued (legacy since
wenzelm@55152	2375	Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context
wenzelm@55152	2376	where instantiations with schematic variables are intended (for
wenzelm@55152	2377	declaration commands like 'lemmas' or attributes like "of"). The
wenzelm@55152	2378	following temporary definition may help to port old applications:
wenzelm@55152	2379
wenzelm@55152	2380	attribute_setup standard =
wenzelm@55152	2381	"Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
wenzelm@55152	2382
wenzelm@55001	2383	* More thorough check of proof context for goal statements and
wenzelm@55006	2384	attributed fact expressions (concerning background theory, declared
wenzelm@55006	2385	hyps). Potential INCOMPATIBILITY, tools need to observe standard
wenzelm@55006	2386	context discipline. See also Assumption.add_assumes and the more
wenzelm@55006	2387	primitive Thm.assume_hyps.
wenzelm@55001	2388
wenzelm@55108	2389	* Inner syntax token language allows regular quoted strings "..."
wenzelm@55108	2390	(only makes sense in practice, if outer syntax is delimited
wenzelm@57452	2391	differently, e.g. via cartouches).
wenzelm@57452	2392
wenzelm@57504	2393	* Command 'print_term_bindings' supersedes 'print_binds' for clarity,
wenzelm@57504	2394	but the latter is retained some time as Proof General legacy.
wenzelm@57504	2395
wenzelm@57452	2396	* Code generator preprocessor: explicit control of simp tracing on a
wenzelm@57452	2397	per-constant basis. See attribute "code_preproc".
haftmann@57430	2398
wenzelm@55001	2399
haftmann@54227	2400	* HOL *
haftmann@54227	2401
wenzelm@57504	2402	* Code generator: enforce case of identifiers only for strict target
wenzelm@57504	2403	language requirements. INCOMPATIBILITY.
wenzelm@57504	2404
wenzelm@57504	2405	* Code generator: explicit proof contexts in many ML interfaces.
wenzelm@57504	2406	INCOMPATIBILITY.
wenzelm@57504	2407
wenzelm@57504	2408	* Code generator: minimize exported identifiers by default. Minor
wenzelm@57504	2409	INCOMPATIBILITY.
wenzelm@57504	2410
wenzelm@57504	2411	* Code generation for SML and OCaml: dropped arcane "no_signatures"
wenzelm@57504	2412	option. Minor INCOMPATIBILITY.
wenzelm@57504	2413
wenzelm@57504	2414	* "declare [[code abort: ...]]" replaces "code_abort ...".
wenzelm@57504	2415	INCOMPATIBILITY.
wenzelm@57504	2416
wenzelm@57504	2417	* "declare [[code drop: ...]]" drops all code equations associated
wenzelm@57504	2418	with the given constants.
wenzelm@57504	2419
wenzelm@57504	2420	* Code generations are provided for make, fields, extend and truncate
wenzelm@57504	2421	operations on records.
haftmann@57437	2422
wenzelm@57452	2423	* Command and antiquotation "value" are now hardcoded against nbe and
wenzelm@57452	2424	ML. Minor INCOMPATIBILITY.
wenzelm@57452	2425
wenzelm@57504	2426	* Renamed command 'enriched_type' to 'functor'. INCOMPATIBILITY.
wenzelm@57504	2427
wenzelm@57504	2428	* The symbol "\<newline>" may be used within char or string literals
wenzelm@57504	2429	to represent (Char Nibble0 NibbleA), i.e. ASCII newline.
wenzelm@57504	2430
wenzelm@57504	2431	* Qualified String.implode and String.explode. INCOMPATIBILITY.
haftmann@56923	2432
wenzelm@57452	2433	* Simplifier: Enhanced solver of preconditions of rewrite rules can
wenzelm@57452	2434	now deal with conjunctions. For help with converting proofs, the old
wenzelm@57452	2435	behaviour of the simplifier can be restored like this: declare/using
wenzelm@57452	2436	[[simp_legacy_precond]]. This configuration option will disappear
wenzelm@57452	2437	again in the future. INCOMPATIBILITY.
nipkow@56073	2438
wenzelm@55139	2439	* Simproc "finite_Collect" is no longer enabled by default, due to
wenzelm@55139	2440	spurious crashes and other surprises. Potential INCOMPATIBILITY.
wenzelm@55139	2441
wenzelm@57452	2442	* Moved new (co)datatype package and its dependencies from session
wenzelm@57452	2443	"HOL-BNF" to "HOL". The commands 'bnf', 'wrap_free_constructors',
wenzelm@57452	2444	'datatype_new', 'codatatype', 'primcorec', 'primcorecursive' are now
wenzelm@57452	2445	part of theory "Main".
wenzelm@57452	2446
blanchet@55098	2447	Theory renamings:
blanchet@55098	2448	FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
blanchet@55098	2449	Library/Wfrec.thy ~> Wfrec.thy
blanchet@55098	2450	Library/Zorn.thy ~> Zorn.thy
blanchet@55098	2451	Cardinals/Order_Relation.thy ~> Order_Relation.thy
blanchet@55098	2452	Library/Order_Union.thy ~> Cardinals/Order_Union.thy
blanchet@55098	2453	Cardinals/Cardinal_Arithmetic_Base.thy ~> BNF_Cardinal_Arithmetic.thy
blanchet@55098	2454	Cardinals/Cardinal_Order_Relation_Base.thy ~> BNF_Cardinal_Order_Relation.thy
blanchet@55098	2455	Cardinals/Constructions_on_Wellorders_Base.thy ~> BNF_Constructions_on_Wellorders.thy
blanchet@55098	2456	Cardinals/Wellorder_Embedding_Base.thy ~> BNF_Wellorder_Embedding.thy
blanchet@55098	2457	Cardinals/Wellorder_Relation_Base.thy ~> BNF_Wellorder_Relation.thy
blanchet@55098	2458	BNF/Ctr_Sugar.thy ~> Ctr_Sugar.thy
blanchet@55098	2459	BNF/Basic_BNFs.thy ~> Basic_BNFs.thy
blanchet@55098	2460	BNF/BNF_Comp.thy ~> BNF_Comp.thy
blanchet@55098	2461	BNF/BNF_Def.thy ~> BNF_Def.thy
blanchet@55098	2462	BNF/BNF_FP_Base.thy ~> BNF_FP_Base.thy
blanchet@55098	2463	BNF/BNF_GFP.thy ~> BNF_GFP.thy
blanchet@55098	2464	BNF/BNF_LFP.thy ~> BNF_LFP.thy
blanchet@55098	2465	BNF/BNF_Util.thy ~> BNF_Util.thy
blanchet@55098	2466	BNF/Coinduction.thy ~> Coinduction.thy
blanchet@55098	2467	BNF/More_BNFs.thy ~> Library/More_BNFs.thy
blanchet@55098	2468	BNF/Countable_Type.thy ~> Library/Countable_Set_Type.thy
blanchet@55098	2469	BNF/Examples/* ~> BNF_Examples/*
wenzelm@57452	2470
blanchet@55098	2471	New theories:
blanchet@55098	2472	Wellorder_Extension.thy (split from Zorn.thy)
blanchet@55098	2473	Library/Cardinal_Notations.thy
traytel@56942	2474	Library/BNF_Axomatization.thy
blanchet@55098	2475	BNF_Examples/Misc_Primcorec.thy
blanchet@55098	2476	BNF_Examples/Stream_Processor.thy
wenzelm@57452	2477
blanchet@55519	2478	Discontinued theories:
blanchet@55098	2479	BNF/BNF.thy
blanchet@55098	2480	BNF/Equiv_Relations_More.thy
wenzelm@57452	2481
wenzelm@57452	2482	INCOMPATIBILITY.
blanchet@55098	2483
blanchet@56118	2484	* New (co)datatype package:
wenzelm@57452	2485	- Command 'primcorec' is fully implemented.
wenzelm@57452	2486	- Command 'datatype_new' generates size functions ("size_xxx" and
wenzelm@57452	2487	"size") as required by 'fun'.
wenzelm@57452	2488	- BNFs are integrated with the Lifting tool and new-style
wenzelm@57452	2489	(co)datatypes with Transfer.
wenzelm@57452	2490	- Renamed commands:
blanchet@55875	2491	datatype_new_compat ~> datatype_compat
blanchet@55875	2492	primrec_new ~> primrec
blanchet@55875	2493	wrap_free_constructors ~> free_constructors
blanchet@55875	2494	INCOMPATIBILITY.
wenzelm@57452	2495	- The generated constants "xxx_case" and "xxx_rec" have been renamed
blanchet@55875	2496	"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
blanchet@55875	2497	INCOMPATIBILITY.
wenzelm@57452	2498	- The constant "xxx_(un)fold" and related theorems are no longer
wenzelm@57452	2499	generated. Use "xxx_(co)rec" or define "xxx_(un)fold" manually
wenzelm@57452	2500	using "prim(co)rec".
blanchet@55875	2501	INCOMPATIBILITY.
wenzelm@57452	2502	- No discriminators are generated for nullary constructors by
wenzelm@57452	2503	default, eliminating the need for the odd "=:" syntax.
blanchet@57091	2504	INCOMPATIBILITY.
wenzelm@57452	2505	- No discriminators or selectors are generated by default by
blanchet@57094	2506	"datatype_new", unless custom names are specified or the new
blanchet@57094	2507	"discs_sels" option is passed.
blanchet@57094	2508	INCOMPATIBILITY.
blanchet@55875	2509
blanchet@55643	2510	* Old datatype package:
wenzelm@57452	2511	- The generated theorems "xxx.cases" and "xxx.recs" have been
wenzelm@57452	2512	renamed "xxx.case" and "xxx.rec" (e.g., "sum.cases" ->
wenzelm@57452	2513	"sum.case"). INCOMPATIBILITY.
wenzelm@57452	2514	- The generated constants "xxx_case", "xxx_rec", and "xxx_size" have
wenzelm@57452	2515	been renamed "case_xxx", "rec_xxx", and "size_xxx" (e.g.,
wenzelm@57452	2516	"prod_case" ~> "case_prod"). INCOMPATIBILITY.
wenzelm@57452	2517
wenzelm@57452	2518	* The types "'a list" and "'a option", their set and map functions,
wenzelm@57452	2519	their relators, and their selectors are now produced using the new
wenzelm@57452	2520	BNF-based datatype package.
wenzelm@57452	2521
blanchet@55519	2522	Renamed constants:
blanchet@55519	2523	Option.set ~> set_option
blanchet@55519	2524	Option.map ~> map_option
blanchet@55525	2525	option_rel ~> rel_option
wenzelm@57452	2526
blanchet@55519	2527	Renamed theorems:
blanchet@55585	2528	set_def ~> set_rec[abs_def]
blanchet@55519	2529	map_def ~> map_rec[abs_def]
blanchet@55519	2530	Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
blanchet@56652	2531	option.recs ~> option.rec
blanchet@55524	2532	list_all2_def ~> list_all2_iff
blanchet@55585	2533	set.simps ~> set_simps (or the slightly different "list.set")
blanchet@55519	2534	map.simps ~> list.map
blanchet@55519	2535	hd.simps ~> list.sel(1)
blanchet@55519	2536	tl.simps ~> list.sel(2-3)
blanchet@55519	2537	the.simps ~> option.sel
wenzelm@57452	2538
wenzelm@57452	2539	INCOMPATIBILITY.
blanchet@55519	2540
blanchet@55933	2541	* The following map functions and relators have been renamed:
blanchet@55939	2542	sum_map ~> map_sum
blanchet@55939	2543	map_pair ~> map_prod
blanchet@55944	2544	prod_rel ~> rel_prod
blanchet@55943	2545	sum_rel ~> rel_sum
blanchet@55945	2546	fun_rel ~> rel_fun
blanchet@55942	2547	set_rel ~> rel_set
blanchet@55942	2548	filter_rel ~> rel_filter
wenzelm@57452	2549	fset_rel ~> rel_fset (in "src/HOL/Library/FSet.thy")
wenzelm@57452	2550	cset_rel ~> rel_cset (in "src/HOL/Library/Countable_Set_Type.thy")
wenzelm@57452	2551	vset ~> rel_vset (in "src/HOL/Library/Quotient_Set.thy")
wenzelm@57452	2552
wenzelm@57452	2553	INCOMPATIBILITY.
wenzelm@57452	2554
kuncar@57826	2555	* Lifting and Transfer:
kuncar@57826	2556	- a type variable as a raw type is supported
kuncar@57826	2557	- stronger reflexivity prover
kuncar@57826	2558	- rep_eq is always generated by lift_definition
wenzelm@57856	2559	- setup for Lifting/Transfer is now automated for BNFs
kuncar@57826	2560	+ holds for BNFs that do not contain a dead variable
wenzelm@57856	2561	+ relator_eq, relator_mono, relator_distr, relator_domain,
kuncar@57826	2562	relator_eq_onp, quot_map, transfer rules for bi_unique, bi_total,
kuncar@57826	2563	right_unique, right_total, left_unique, left_total are proved
kuncar@57826	2564	automatically
kuncar@57826	2565	+ definition of a predicator is generated automatically
kuncar@57826	2566	+ simplification rules for a predicator definition are proved
kuncar@57826	2567	automatically for datatypes
kuncar@57826	2568	- consolidation of the setup of Lifting/Transfer
wenzelm@57856	2569	+ property that a relator preservers reflexivity is not needed any
kuncar@57826	2570	more
kuncar@57826	2571	Minor INCOMPATIBILITY.
wenzelm@57856	2572	+ left_total and left_unique rules are now transfer rules
kuncar@57826	2573	(reflexivity_rule attribute not needed anymore)
kuncar@57826	2574	INCOMPATIBILITY.
wenzelm@57856	2575	+ Domainp does not have to be a separate assumption in
kuncar@57826	2576	relator_domain theorems (=> more natural statement)
kuncar@57826	2577	INCOMPATIBILITY.
kuncar@57826	2578	- registration of code equations is more robust
kuncar@57826	2579	Potential INCOMPATIBILITY.
kuncar@57826	2580	- respectfulness proof obligation is preprocessed to a more readable
kuncar@57826	2581	form
kuncar@57826	2582	Potential INCOMPATIBILITY.
kuncar@57826	2583	- eq_onp is always unfolded in respectfulness proof obligation
kuncar@57826	2584	Potential INCOMPATIBILITY.
wenzelm@57856	2585	- unregister lifting setup for Code_Numeral.integer and
kuncar@57826	2586	Code_Numeral.natural
kuncar@57826	2587	Potential INCOMPATIBILITY.
kuncar@57826	2588	- Lifting.invariant -> eq_onp
kuncar@57826	2589	INCOMPATIBILITY.
wenzelm@57856	2590
wenzelm@57508	2591	* New internal SAT solver "cdclite" that produces models and proof
wenzelm@57508	2592	traces. This solver replaces the internal SAT solvers "enumerate" and
wenzelm@57508	2593	"dpll". Applications that explicitly used one of these two SAT
wenzelm@57508	2594	solvers should use "cdclite" instead. In addition, "cdclite" is now
wenzelm@57508	2595	the default SAT solver for the "sat" and "satx" proof methods and
wenzelm@57508	2596	corresponding tactics; the old default can be restored using "declare
wenzelm@57508	2597	[[sat_solver = zchaff_with_proofs]]". Minor INCOMPATIBILITY.
wenzelm@57508	2598
wenzelm@57508	2599	* SMT module: A new version of the SMT module, temporarily called
wenzelm@57508	2600	"SMT2", uses SMT-LIB 2 and supports recent versions of Z3 (e.g.,
wenzelm@57508	2601	4.3). The new proof method is called "smt2". CVC3 and CVC4 are also
wenzelm@57508	2602	supported as oracles. Yices is no longer supported, because no version
wenzelm@57508	2603	of the solver can handle both SMT-LIB 2 and quantifiers.
wenzelm@57508	2604
wenzelm@57508	2605	* Activation of Z3 now works via "z3_non_commercial" system option
wenzelm@57508	2606	(without requiring restart), instead of former settings variable
wenzelm@57508	2607	"Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu
wenzelm@57508	2608	Plugin Options / Isabelle / General.
wenzelm@57508	2609
wenzelm@57508	2610	* Sledgehammer:
wenzelm@57508	2611	- Z3 can now produce Isar proofs.
wenzelm@57508	2612	- MaSh overhaul:
blanchet@57532	2613	. New SML-based learning algorithms eliminate the dependency on
wenzelm@57508	2614	Python and increase performance and reliability.
wenzelm@57508	2615	. MaSh and MeSh are now used by default together with the
wenzelm@57508	2616	traditional MePo (Meng-Paulson) relevance filter. To disable
wenzelm@57508	2617	MaSh, set the "MaSh" system option in Isabelle/jEdit Plugin
wenzelm@57508	2618	Options / Isabelle / General to "none".
wenzelm@57508	2619	- New option:
wenzelm@57508	2620	smt_proofs
wenzelm@57508	2621	- Renamed options:
wenzelm@57508	2622	isar_compress ~> compress
wenzelm@57508	2623	isar_try0 ~> try0
wenzelm@57508	2624
wenzelm@57508	2625	INCOMPATIBILITY.
wenzelm@57508	2626
wenzelm@57508	2627	* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
wenzelm@57508	2628
wenzelm@57508	2629	* Nitpick:
wenzelm@57508	2630	- Fixed soundness bug whereby mutually recursive datatypes could
wenzelm@57508	2631	take infinite values.
wenzelm@57508	2632	- Fixed soundness bug with low-level number functions such as
wenzelm@57508	2633	"Abs_Integ" and "Rep_Integ".
wenzelm@57508	2634	- Removed "std" option.
wenzelm@57508	2635	- Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
wenzelm@57508	2636	"hide_types".
wenzelm@57508	2637
wenzelm@57508	2638	* Metis: Removed legacy proof method 'metisFT'. Use 'metis
wenzelm@57508	2639	(full_types)' instead. INCOMPATIBILITY.
wenzelm@57508	2640
wenzelm@57508	2641	* Try0: Added 'algebra' and 'meson' to the set of proof methods.
wenzelm@57508	2642
wenzelm@57508	2643	* Adjustion of INF and SUP operations:
wenzelm@57508	2644	- Elongated constants INFI and SUPR to INFIMUM and SUPREMUM.
wenzelm@57508	2645	- Consolidated theorem names containing INFI and SUPR: have INF and
wenzelm@57508	2646	SUP instead uniformly.
wenzelm@57508	2647	- More aggressive normalization of expressions involving INF and Inf
wenzelm@57508	2648	or SUP and Sup.
wenzelm@57508	2649	- INF_image and SUP_image do not unfold composition.
wenzelm@57508	2650	- Dropped facts INF_comp, SUP_comp.
wenzelm@57508	2651	- Default congruence rules strong_INF_cong and strong_SUP_cong, with
wenzelm@57508	2652	simplifier implication in premises. Generalize and replace former
wenzelm@57508	2653	INT_cong, SUP_cong
wenzelm@57508	2654
wenzelm@57508	2655	INCOMPATIBILITY.
wenzelm@57508	2656
wenzelm@57508	2657	* SUP and INF generalized to conditionally_complete_lattice.
wenzelm@57508	2658
wenzelm@57508	2659	* Swapped orientation of facts image_comp and vimage_comp:
wenzelm@57508	2660
wenzelm@57508	2661	image_compose ~> image_comp [symmetric]
wenzelm@57508	2662	image_comp ~> image_comp [symmetric]
wenzelm@57508	2663	vimage_compose ~> vimage_comp [symmetric]
wenzelm@57508	2664	vimage_comp ~> vimage_comp [symmetric]
wenzelm@57508	2665
wenzelm@57508	2666	INCOMPATIBILITY.
wenzelm@57508	2667
wenzelm@57504	2668	* Theory reorganization: split of Big_Operators.thy into
wenzelm@57504	2669	Groups_Big.thy and Lattices_Big.thy.
blanchet@55098	2670
haftmann@57418	2671	* Consolidated some facts about big group operators:
haftmann@57418	2672
haftmann@57418	2673	setsum_0' ~> setsum.neutral
haftmann@57418	2674	setsum_0 ~> setsum.neutral_const
haftmann@57418	2675	setsum_addf ~> setsum.distrib
haftmann@57418	2676	setsum_cartesian_product ~> setsum.cartesian_product
haftmann@57418	2677	setsum_cases ~> setsum.If_cases
haftmann@57418	2678	setsum_commute ~> setsum.commute
haftmann@57418	2679	setsum_cong ~> setsum.cong
haftmann@57418	2680	setsum_delta ~> setsum.delta
haftmann@57418	2681	setsum_delta' ~> setsum.delta'
haftmann@57418	2682	setsum_diff1' ~> setsum.remove
haftmann@57418	2683	setsum_empty ~> setsum.empty
haftmann@57418	2684	setsum_infinite ~> setsum.infinite
haftmann@57418	2685	setsum_insert ~> setsum.insert
haftmann@57418	2686	setsum_inter_restrict'' ~> setsum.inter_filter
haftmann@57418	2687	setsum_mono_zero_cong_left ~> setsum.mono_neutral_cong_left
haftmann@57418	2688	setsum_mono_zero_cong_right ~> setsum.mono_neutral_cong_right
haftmann@57418	2689	setsum_mono_zero_left ~> setsum.mono_neutral_left
haftmann@57418	2690	setsum_mono_zero_right ~> setsum.mono_neutral_right
haftmann@57418	2691	setsum_reindex ~> setsum.reindex
haftmann@57418	2692	setsum_reindex_cong ~> setsum.reindex_cong
haftmann@57418	2693	setsum_reindex_nonzero ~> setsum.reindex_nontrivial
haftmann@57418	2694	setsum_restrict_set ~> setsum.inter_restrict
haftmann@57418	2695	setsum_Plus ~> setsum.Plus
haftmann@57418	2696	setsum_setsum_restrict ~> setsum.commute_restrict
haftmann@57418	2697	setsum_Sigma ~> setsum.Sigma
haftmann@57418	2698	setsum_subset_diff ~> setsum.subset_diff
haftmann@57418	2699	setsum_Un_disjoint ~> setsum.union_disjoint
haftmann@57418	2700	setsum_UN_disjoint ~> setsum.UNION_disjoint
haftmann@57418	2701	setsum_Un_Int ~> setsum.union_inter
haftmann@57418	2702	setsum_Union_disjoint ~> setsum.Union_disjoint
haftmann@57418	2703	setsum_UNION_zero ~> setsum.Union_comp
haftmann@57418	2704	setsum_Un_zero ~> setsum.union_inter_neutral
haftmann@57418	2705	strong_setprod_cong ~> setprod.strong_cong
haftmann@57418	2706	strong_setsum_cong ~> setsum.strong_cong
haftmann@57418	2707	setprod_1' ~> setprod.neutral
haftmann@57418	2708	setprod_1 ~> setprod.neutral_const
haftmann@57418	2709	setprod_cartesian_product ~> setprod.cartesian_product
haftmann@57418	2710	setprod_cong ~> setprod.cong
haftmann@57418	2711	setprod_delta ~> setprod.delta
haftmann@57418	2712	setprod_delta' ~> setprod.delta'
haftmann@57418	2713	setprod_empty ~> setprod.empty
haftmann@57418

author	wenzelm
	Mon Sep 05 23:39:15 2016 +0200 (2016-09-05)
changeset 63807	5f77017055a3
parent 63795	7f6128adfe67
child 63821	52235c27538c
permissions	-rw-r--r--