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.6  
     1.7 -ML {*AtpThread.problem_name := "set__equal_union"*}
     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.14  
    1.15  
    1.16 -ML {*AtpThread.problem_name := "set__equal_inter"*}
    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.21  
    1.22 -ML {*AtpThread.problem_name := "set__fixedpoint"*}
    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
    1.30  
    1.31 -ML {*AtpThread.problem_name := "set__singleton_example"*}
    1.32 +ML {*AtpWrapper.problem_name := "set__singleton_example"*}
    1.33  lemma (*singleton_example_2:*)
    1.34       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    1.35  by (metis Set.subsetI Union_upper insertCI set_eq_subset)
    1.36 @@ -260,7 +260,7 @@
    1.37    293-314.
    1.38  *}
    1.39  
    1.40 -ML {*AtpThread.problem_name := "set__Bledsoe_Fung"*}
    1.41 +ML {*AtpWrapper.problem_name := "set__Bledsoe_Fung"*}
    1.42  (*Notes: 1, the numbering doesn't completely agree with the paper. 
    1.43  2, we must rename set variables to avoid type clashes.*)
    1.44  lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"