# HG changeset patch
# User wenzelm
# Date 1129911276 -7200
# Node ID d31acb64aa9a4e4dc733a70b2c8d3d1ec7a22e1d
# Parent  369e2af8ee458b3bfa7238806f135c85704b4342
avoid home-grown meta_allE;

diff -r 369e2af8ee45 -r d31acb64aa9a src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Oct 21 18:14:34 2005 +0200
+++ b/src/HOL/Record.thy	Fri Oct 21 18:14:36 2005 +0200
@@ -8,13 +8,6 @@
 uses ("Tools/record_package.ML")
 begin
 
-ML {*
-val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
-by (rtac h2 1);
-by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
-qed "meta_allE";
-*}
-
 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   by simp