doc-src/Tutorial/Misc/ROOT.ML

inj is now a translation of inj_on

use_thy "Tree";

context Main.thy;
use"exhaust.ML";
use"autotac.ML";
result();

use_thy"NatSum";
result();

use_thy"Types";
use_thy"Defs";
use_thy"ConstDefs";

context Main.thy;
Goal "! xs. if xs = [] then rev xs = [] else rev xs ~= []";
use"splitif.ML";

Goal "(case xs of [] => zs | y#ys => y#(ys@zs)) = xs@zs";
use"splitlist.ML";

use_thy "Itrev";
use "itrev1.ML";
use "itrev2.ML";
use "itrev3.ML";
use "induct_auto.ML";
result();