Changes

Summary

hooks for foundational terms: protection of foundational terms during simplification
merged
merged
avoid deprecated operations;
tuned -- avoid odd compiler warning;
avoid deprecated operations;
deprecated and obsolete;
tuned signature -- avoid warnings;
more informative error;
new funs successive and distinct_adj
added lemmas

Changeset 71788:ca3ac5238c41 by haftmann: hooks for foundational terms: protection of foundational terms during simplification
The file was modified	`NEWS` (diff)
The file was modified	`src/Pure/Isar/generic_target.ML` (diff)
The file was modified	`src/Pure/simplifier.ML` (diff)
Changeset 71787:acfe72ff00c2 by wenzelm: merged
Changeset 71786:97975476547c by wenzelm: merged
Changeset 71785:39613d6e2021 by wenzelm: avoid deprecated operations;
The file was modified	`src/Pure/General/timing.scala` (diff)
Changeset 71784:8a5da740e388 by wenzelm: tuned -- avoid odd compiler warning;
The file was modified	`src/Pure/Thy/latex.scala` (diff)
Changeset 71783:73dee865d567 by wenzelm: avoid deprecated operations;
The file was modified	`src/Tools/jEdit/src/fold_handling.scala` (diff)
The file was modified	`src/Tools/jEdit/src/keymap_merge.scala` (diff)
The file was modified	`src/Tools/jEdit/src/rich_text_area.scala` (diff)
The file was modified	`src/Tools/jEdit/src/token_markup.scala` (diff)
Changeset 71782:a57035ae9029 by wenzelm: deprecated and obsolete;
The file was modified	`src/Tools/jEdit/src/scala_console.scala` (diff)
Changeset 71781:3fd54f7f52b0 by wenzelm: tuned signature -- avoid warnings;
The file was modified	`src/Pure/General/pretty.scala` (diff)
The file was modified	`src/Pure/term.scala` (diff)
Changeset 71780:21adf2ed442c by wenzelm: more informative error;
The file was modified	`src/Pure/General/ssh.scala` (diff)
Changeset 71779:3ab4b989f8c8 by nipkow: new funs successive and distinct_adj
The file was modified	`src/HOL/List.thy` (diff)
Changeset 71778:ad91684444d7 by nipkow: added lemmas
The file was modified	`src/HOL/List.thy` (diff)