src/HOL/Record.thy
changeset 17957 d31acb64aa9a
parent 16417 9bc16273c2d4
child 21226 a607ae87ee81
     1.1 --- a/src/HOL/Record.thy	Fri Oct 21 18:14:34 2005 +0200
     1.2 +++ b/src/HOL/Record.thy	Fri Oct 21 18:14:36 2005 +0200
     1.3 @@ -8,13 +8,6 @@
     1.4  uses ("Tools/record_package.ML")
     1.5  begin
     1.6  
     1.7 -ML {*
     1.8 -val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
     1.9 -by (rtac h2 1);
    1.10 -by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
    1.11 -qed "meta_allE";
    1.12 -*}
    1.13 -
    1.14  lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
    1.15    by simp
    1.16