src/HOL/MetisExamples/set.thy
 changeset 28592 824f8390aaa2 parent 28486 873726bdfd47 child 32519 e9644b497e1c
1.1 --- a/src/HOL/MetisExamples/set.thy	Tue Oct 14 15:45:46 2008 +0200
1.2 +++ b/src/HOL/MetisExamples/set.thy	Tue Oct 14 16:01:36 2008 +0200
1.3 @@ -198,7 +198,7 @@
1.4    by (metis 11 6 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq 9 Un_upper2 sup_set_eq 1 sup_set_eq Un_upper1 sup_set_eq 0 sup_set_eq)
1.5  qed
1.8 +ML {*AtpWrapper.problem_name := "set__equal_union"*}
1.9  lemma (*equal_union: *)
1.10     "(X = Y \<union> Z) =
1.11      (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
1.12 @@ -206,12 +206,12 @@
1.13  by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
1.17 +ML {*AtpWrapper.problem_name := "set__equal_inter"*}
1.18  lemma "(X = Y \<inter> Z) =
1.19      (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
1.20  by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
1.23 +ML {*AtpWrapper.problem_name := "set__fixedpoint"*}
1.24  lemma fixedpoint:
1.25      "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
1.26  by metis
1.27 @@ -230,7 +230,7 @@
1.28    by (metis 4 0)
1.29  qed