Wishes for the Isabelle proof assistant

Isabelle/HOL

The datatype package could automatically generate the following lemma.

lemma list_map_eq_imp_rel:
  shows "map f xs = map g ys ⟷ list_all2 (λx y. f x = g y) xs ys"
proof
  assume assms: "map f xs = map g ys"
  hence "length xs = length ys"
    by (metis length_map)
  thus "list_all2 (λx y. f x = g y) xs ys"
    unfolding list_all2_conv_all_nth
    using assms
    by (auto intro: map_eq_imp_length_eq simp: nth_map[of _ xs f, symmetric])
next
  assume "list_all2 (λx y. f x = g y) xs ys"
  thus "map f xs = map g ys"
    by (induction xs ys rule: list.rel_induct; simp)
qed

Isabelle/Isar

A tactic that takes one or more tactics as parameter, execute them independently on the current subgoals, and print their respective running times in the output window. The goal is to find out which tactic is the fastest, so it is ok if the output is undefined in case they don't achieve the same result. It would be even better if statistics on memory consumption was printed.
When extending a locale, I want to be able to instanciate the type variables of the locale predicate. e.g.
```
locale A =
  fixes foo :: "'a => 'b => nat"

locale B =
  A1: A[where 'a = 'aa and 'b = 'bb] foo1 +
  A2: A[where 'a = 'cc and 'b = 'bb] foo2
  for foo1 and foo2
```
The alternative is to write type annotations on the constants in the for clause, which gets very verbose for big locales.
When refering to a named locale instatiation, I want to be able to refer to the locale's parameters in the user-defined namespace in addition to the concrete constant name. e.g.
```
locale A =
  fixes foo :: "'a => 'b => nat"

locale B =
  namespace: A concretefoo +
  assumes somelemma: "... namespace.foo ... concretefoo ..."
```

In a local context, I want to be able to define type synonyms that refer to the context's type variables. e.g.

datatype ('a, 'b, 'c) sometype = MkSomeType 'a 'b 'c

context
  fixes foo :: "'a => 'b => 'c => bool"
begin

type_synonym mytype = "('a, 'b, 'c) sometype"

end

IDE

Automatic generation of cases when defining a primitively recursive function.

Document preparation system

An antiquotation to insert an existing locale definition defined in an imported theory.

Build system

An option that would, in conjunction with the -v option, print the verification time of the individual theories, and not just of the session.
When using the -v option, the theories should be only displayed when their verification successfully completed, and not when it starts as is now the case.