moved after method.ML;
moved FINDGOAL/HEADGOAL to method.ML;
moved type method to method.ML;
prepare attributes here;
tuned various interfaces (cf. isar_thy.ML);
tuned;
L2 = Base +
rules
pi_bs "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
lam_bs "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
==> Abs(A,f) : Prod(A,B)"
end