[isabelle] schematic variables



Hello,

  I wonder if it is possible to instantiate schematic variables
after unfolding (see example below).
thanks

Mamoun

--------

definition "ref P Q = (\<forall> s. P s \<longrightarrow> Q s)"

theorem
  assumes r1: "ref A A'"
  assumes r2: "ref B B'"
shows "ref (A \<union> B) (A' \<union> B')"
proof -
have "?thesis" unfolding ref_def (* is "\<forall> s. ?L s \<longrightarrow> ?R s" *)

begin:vcard
fn:Mamoun FILALI-AMINE
n:FILALI-AMINE;Mamoun
adr;quoted-printable:118 Route de Narbonne;;IRIT Universit=C3=A9 Paul Sabatier;Toulouse;;31062 cedex 9;France
email;internet:filali at irit.fr
tel;work:00 33 5 61 55 69 26
tel;fax:00 33 5 61 55 64 48
version:2.1
end:vcard



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.