doc-src/TutorialI/ToyList2/ToyList1

Sort search results in order of relevance, where relevance =
a) better if 0 premises for intro or 1 premise for elim/dest rules
b) better if substitution size wrt to current goal is smaller

Only applies to intro, dest, elim, and simp

(contributed by Rafal Kolanski, NICTA)

theory ToyList
imports PreList
begin

datatype 'a list = Nil                          ("[]")
                 | Cons 'a "'a list"            (infixr "#" 65)

consts app :: "'a list => 'a list => 'a list"   (infixr "@" 65)
       rev :: "'a list => 'a list"

primrec
"[] @ ys       = ys"
"(x # xs) @ ys = x # (xs @ ys)"

primrec
"rev []        = []"
"rev (x # xs)  = (rev xs) @ (x # [])"