# HG changeset patch
# User blanchet
# Date 1348699251 -7200
# Node ID ba31032887db3763d04994cf8fba12ab74ffe95d
# Parent  e716209814b39652be593f0d4d39c6338b12d94c
modernized examples;
removed now trivial "HFset"

diff -r e716209814b3 -r ba31032887db src/HOL/BNF/Examples/HFset.thy
--- a/src/HOL/BNF/Examples/HFset.thy	Wed Sep 26 19:50:10 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      HOL/BNF/Examples/HFset.thy
-    Author:     Andrei Popescu, TU Muenchen
-    Copyright   2012
-
-Hereditary sets.
-*)
-
-header {* Hereditary Sets *}
-
-theory HFset
-imports "../BNF"
-begin
-
-
-section {* Datatype definition *}
-
-data_raw hfset: 'hfset = "'hfset fset"
-
-
-section {* Customization of terms *}
-
-subsection{* Constructors *}
-
-definition "Fold hs \<equiv> hfset_ctor hs"
-
-lemma hfset_simps[simp]:
-"\<And>hs1 hs2. Fold hs1 = Fold hs2 \<longrightarrow> hs1 = hs2"
-unfolding Fold_def hfset.ctor_inject by auto
-
-theorem hfset_cases[elim, case_names Fold]:
-assumes Fold: "\<And> hs. h = Fold hs \<Longrightarrow> phi"
-shows phi
-using Fold unfolding Fold_def
-by (cases rule: hfset.ctor_exhaust[of h]) simp
-
-lemma hfset_induct[case_names Fold, induct type: hfset]:
-assumes Fold: "\<And> hs. (\<And> h. h |\<in>| hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
-shows "phi t"
-apply (induct rule: hfset.ctor_induct)
-using Fold unfolding Fold_def fset_fset_member mem_Collect_eq ..
-
-(* alternative induction principle, using fset: *)
-lemma hfset_induct_fset[case_names Fold, induct type: hfset]:
-assumes Fold: "\<And> hs. (\<And> h. h \<in> fset hs \<Longrightarrow> phi h) \<Longrightarrow> phi (Fold hs)"
-shows "phi t"
-apply (induct rule: hfset_induct)
-using Fold by (metis notin_fset)
-
-subsection{* Recursion and iteration (fold) *}
-
-lemma hfset_ctor_rec:
-"hfset_ctor_rec R (Fold hs) = R (map_fset <id, hfset_ctor_rec R> hs)"
-using hfset.ctor_rec unfolding Fold_def .
-
-(* The iterator has a simpler form: *)
-lemma hfset_ctor_fold:
-"hfset_ctor_fold R (Fold hs) = R (map_fset (hfset_ctor_fold R) hs)"
-using hfset.ctor_fold unfolding Fold_def .
-
-end
diff -r e716209814b3 -r ba31032887db src/HOL/BNF/Examples/Lambda_Term.thy
--- a/src/HOL/BNF/Examples/Lambda_Term.thy	Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy	Thu Sep 27 00:40:51 2012 +0200
@@ -15,203 +15,57 @@
 
 section {* Datatype definition *}
 
-data_raw trm: 'trm = "'a + 'trm \<times> 'trm + 'a \<times> 'trm + ('a \<times> 'trm) fset \<times> 'trm"
-
-
-section {* Customization of terms *}
-
-subsection{* Set and map *}
-
-lemma pre_trm_set2_Lt: "pre_trm_set2 (Inr (Inr (Inr (xts, t)))) = snd ` (fset xts) \<union> {t}"
-unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
-by auto
-
-lemma pre_trm_set2_Var: "\<And>x. pre_trm_set2 (Inl x) = {}"
-and pre_trm_set2_App:
-"\<And>t1 t2. pre_trm_set2 (Inr (Inl t1t2)) = {fst t1t2, snd t1t2}"
-and pre_trm_set2_Lam:
-"\<And>x t. pre_trm_set2 (Inr (Inr (Inl (x, t)))) = {t}"
-unfolding pre_trm_set2_def sum_set_defs prod_set_defs collect_def[abs_def]
-by auto
-
-lemma pre_trm_map:
-"\<And> a1. pre_trm_map f1 f2 (Inl a1) = Inl (f1 a1)"
-"\<And> a2 b2. pre_trm_map f1 f2 (Inr (Inl (a2,b2))) = Inr (Inl (f2 a2, f2 b2))"
-"\<And> a1 a2. pre_trm_map f1 f2 (Inr (Inr (Inl (a1,a2)))) = Inr (Inr (Inl (f1 a1, f2 a2)))"
-"\<And> a1a2s a2.
-   pre_trm_map f1 f2 (Inr (Inr (Inr (a1a2s, a2)))) =
-   Inr (Inr (Inr (map_fset (\<lambda> (a1', a2'). (f1 a1', f2 a2')) a1a2s, f2 a2)))"
-unfolding pre_trm_map_def collect_def[abs_def] map_pair_def by auto
+data 'a trm =
+  Var 'a |
+  App "'a trm" "'a trm" |
+  Lam 'a "'a trm" |
+  Lt "('a \<times> 'a trm) fset" "'a trm"
 
 
-subsection{* Constructors *}
-
-definition "Var x \<equiv> trm_ctor (Inl x)"
-definition "App t1 t2 \<equiv> trm_ctor (Inr (Inl (t1,t2)))"
-definition "Lam x t \<equiv> trm_ctor (Inr (Inr (Inl (x,t))))"
-definition "Lt xts t \<equiv> trm_ctor (Inr (Inr (Inr (xts,t))))"
-
-lemmas ctor_defs = Var_def App_def Lam_def Lt_def
-
-theorem trm_simps[simp]:
-"\<And>x y. Var x = Var y \<longleftrightarrow> x = y"
-"\<And>t1 t2 t1' t2'. App t1 t2 = App t1' t2' \<longleftrightarrow> t1 = t1' \<and> t2 = t2'"
-"\<And>x x' t t'. Lam x t = Lam x' t' \<longleftrightarrow> x = x' \<and> t = t'"
-"\<And> xts xts' t t'. Lt xts t = Lt xts' t' \<longleftrightarrow> xts = xts' \<and> t = t'"
-(*  *)
-"\<And> x t1 t2. Var x \<noteq> App t1 t2"  "\<And>x y t. Var x \<noteq> Lam y t"  "\<And> x xts t. Var x \<noteq> Lt xts t"
-"\<And> t1 t2 x t. App t1 t2 \<noteq> Lam x t"  "\<And> t1 t2 xts t. App t1 t2 \<noteq> Lt xts t"
-"\<And>x t xts t1. Lam x t \<noteq> Lt xts t1"
-unfolding ctor_defs trm.ctor_inject by auto
-
-theorem trm_cases[elim, case_names Var App Lam Lt]:
-assumes Var: "\<And> x. t = Var x \<Longrightarrow> phi"
-and App: "\<And> t1 t2. t = App t1 t2 \<Longrightarrow> phi"
-and Lam: "\<And> x t1. t = Lam x t1 \<Longrightarrow> phi"
-and Lt: "\<And> xts t1. t = Lt xts t1 \<Longrightarrow> phi"
-shows phi
-proof(cases rule: trm.ctor_exhaust[of t])
-  fix x assume "t = trm_ctor x"
-  thus ?thesis
-  apply(cases x) using Var unfolding ctor_defs apply blast
-  apply(case_tac b) using App unfolding ctor_defs apply(case_tac a, blast)
-  apply(case_tac ba) using Lam unfolding ctor_defs apply(case_tac a, blast)
-  apply(case_tac bb) using Lt unfolding ctor_defs by blast
-qed
+section {* Customi induction rule *}
 
 lemma trm_induct[case_names Var App Lam Lt, induct type: trm]:
-assumes Var: "\<And> (x::'a). phi (Var x)"
+assumes Var: "\<And> x. phi (Var x)"
 and App: "\<And> t1 t2. \<lbrakk>phi t1; phi t2\<rbrakk> \<Longrightarrow> phi (App t1 t2)"
 and Lam: "\<And> x t. phi t \<Longrightarrow> phi (Lam x t)"
 and Lt: "\<And> xts t. \<lbrakk>\<And> x1 t1. (x1,t1) |\<in>| xts \<Longrightarrow> phi t1; phi t\<rbrakk> \<Longrightarrow> phi (Lt xts t)"
 shows "phi t"
-proof(induct rule: trm.ctor_induct)
-  fix u :: "'a + 'a trm \<times> 'a trm + 'a \<times> 'a trm + ('a \<times> 'a trm) fset \<times> 'a trm"
-  assume IH: "\<And>t. t \<in> pre_trm_set2 u \<Longrightarrow> phi t"
-  show "phi (trm_ctor u)"
-  proof(cases u)
-    case (Inl x)
-    show ?thesis using Var unfolding Var_def Inl .
-  next
-    case (Inr uu) note Inr1 = Inr
-    show ?thesis
-    proof(cases uu)
-      case (Inl t1t2)
-      obtain t1 t2 where t1t2: "t1t2 = (t1,t2)" by (cases t1t2, blast)
-      show ?thesis unfolding Inr1 Inl t1t2 App_def[symmetric] apply(rule App)
-      using IH unfolding Inr1 Inl pre_trm_set2_App t1t2 fst_conv snd_conv by blast+
-    next
-      case (Inr uuu) note Inr2 = Inr
-      show ?thesis
-      proof(cases uuu)
-        case (Inl xt)
-        obtain x t where xt: "xt = (x,t)" by (cases xt, blast)
-        show ?thesis unfolding Inr1 Inr2 Inl xt Lam_def[symmetric] apply(rule Lam)
-        using IH unfolding Inr1 Inr2 Inl pre_trm_set2_Lam xt by blast
-      next
-        case (Inr xts_t)
-        obtain xts t where xts_t: "xts_t = (xts,t)" by (cases xts_t, blast)
-        show ?thesis unfolding Inr1 Inr2 Inr xts_t Lt_def[symmetric] apply(rule Lt) using IH
-        unfolding Inr1 Inr2 Inr pre_trm_set2_Lt xts_t fset_fset_member image_def by auto
-      qed
-    qed
-  qed
-qed
-
-
-subsection{* Recursion and iteration (fold) *}
-
-definition
-"sumJoin4 f1 f2 f3 f4 \<equiv>
-\<lambda> k. (case k of
- Inl x1 \<Rightarrow> f1 x1
-|Inr k1 \<Rightarrow> (case k1 of
- Inl ((s2,a2),(t2,b2)) \<Rightarrow> f2 s2 a2 t2 b2
-|Inr k2 \<Rightarrow> (case k2 of Inl (x3,(t3,b3)) \<Rightarrow> f3 x3 t3 b3
-|Inr (xts,(t4,b4)) \<Rightarrow> f4 xts t4 b4)))"
-
-lemma sumJoin4_simps[simp]:
-"\<And>x. sumJoin4 var app lam lt (Inl x) = var x"
-"\<And> t1 a1 t2 a2. sumJoin4 var app lam lt (Inr (Inl ((t1,a1),(t2,a2)))) = app t1 a1 t2 a2"
-"\<And> x t a. sumJoin4 var app lam lt (Inr (Inr (Inl (x,(t,a))))) = lam x t a"
-"\<And> xtas t a. sumJoin4 var app lam lt (Inr (Inr (Inr (xtas,(t,a))))) = lt xtas t a"
-unfolding sumJoin4_def by auto
-
-definition "trmrec var app lam lt \<equiv> trm_ctor_rec (sumJoin4 var app lam lt)"
-
-lemma trmrec_Var[simp]:
-"trmrec var app lam lt (Var x) = var x"
-unfolding trmrec_def Var_def trm.ctor_rec pre_trm_map(1) by simp
-
-lemma trmrec_App[simp]:
-"trmrec var app lam lt (App t1 t2) =
- app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)"
-unfolding trmrec_def App_def trm.ctor_rec pre_trm_map(2) convol_def by simp
-
-lemma trmrec_Lam[simp]:
-"trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)"
-unfolding trmrec_def Lam_def trm.ctor_rec pre_trm_map(3) convol_def by simp
-
-lemma trmrec_Lt[simp]:
-"trmrec var app lam lt (Lt xts t) =
- lt (map_fset (\<lambda> (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)"
-unfolding trmrec_def Lt_def trm.ctor_rec pre_trm_map(4) convol_def by simp
-
-definition
-"sumJoinI4 f1 f2 f3 f4 \<equiv>
-\<lambda> k. (case k of
- Inl x1 \<Rightarrow> f1 x1
-|Inr k1 \<Rightarrow> (case k1 of
- Inl (a2,b2) \<Rightarrow> f2 a2 b2
-|Inr k2 \<Rightarrow> (case k2 of Inl (x3,b3) \<Rightarrow> f3 x3 b3
-|Inr (xts,b4) \<Rightarrow> f4 xts b4)))"
-
-lemma sumJoinI4_simps[simp]:
-"\<And>x. sumJoinI4 var app lam lt (Inl x) = var x"
-"\<And> a1 a2. sumJoinI4 var app lam lt (Inr (Inl (a1,a2))) = app a1 a2"
-"\<And> x a. sumJoinI4 var app lam lt (Inr (Inr (Inl (x,a)))) = lam x a"
-"\<And> xtas a. sumJoinI4 var app lam lt (Inr (Inr (Inr (xtas,a)))) = lt xtas a"
-unfolding sumJoinI4_def by auto
-
-(* The iterator has a simpler, hence more manageable type. *)
-definition "trmfold var app lam lt \<equiv> trm_ctor_fold (sumJoinI4 var app lam lt)"
-
-lemma trmfold_Var[simp]:
-"trmfold var app lam lt (Var x) = var x"
-unfolding trmfold_def Var_def trm.ctor_fold pre_trm_map(1) by simp
-
-lemma trmfold_App[simp]:
-"trmfold var app lam lt (App t1 t2) =
- app (trmfold var app lam lt t1) (trmfold var app lam lt t2)"
-unfolding trmfold_def App_def trm.ctor_fold pre_trm_map(2) by simp
-
-lemma trmfold_Lam[simp]:
-"trmfold var app lam lt (Lam x t) = lam x (trmfold var app lam lt t)"
-unfolding trmfold_def Lam_def trm.ctor_fold pre_trm_map(3) by simp
-
-lemma trmfold_Lt[simp]:
-"trmfold var app lam lt (Lt xts t) =
- lt (map_fset (\<lambda> (x,t). (x,trmfold var app lam lt t)) xts) (trmfold var app lam lt t)"
-unfolding trmfold_def Lt_def trm.ctor_fold pre_trm_map(4) by simp
+apply induct
+apply (rule Var)
+apply (erule App, assumption)
+apply (erule Lam)
+using Lt unfolding fset_fset_member mem_Collect_eq
+apply (rule meta_mp)
+defer
+apply assumption
+apply (erule thin_rl)
+apply assumption
+apply (drule meta_spec)
+apply (drule meta_spec)
+apply (drule meta_mp)
+apply assumption
+apply (auto simp: snds_def)
+done
 
 
 subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
 
-definition "varsOf = trmfold
+definition "varsOf = trm_fold
 (\<lambda> x. {x})
 (\<lambda> X1 X2. X1 \<union> X2)
 (\<lambda> x X. X \<union> {x})
 (\<lambda> xXs Y. Y \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| xXs}))"
 
+thm trm.fold
 lemma varsOf_simps[simp]:
 "varsOf (Var x) = {x}"
 "varsOf (App t1 t2) = varsOf t1 \<union> varsOf t2"
 "varsOf (Lam x t) = varsOf t \<union> {x}"
 "varsOf (Lt xts t) =
  varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,varsOf t1)) xts})"
-unfolding varsOf_def by simp_all
+unfolding varsOf_def by (simp add: map_pair_def)+
 
-definition "fvarsOf = trmfold
+definition "fvarsOf = trm_fold
 (\<lambda> x. {x})
 (\<lambda> X1 X2. X1 \<union> X2)
 (\<lambda> x X. X - {x})
@@ -225,7 +79,7 @@
  fvarsOf t
  - {x | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
  \<union> (\<Union> {X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
-unfolding fvarsOf_def by simp_all
+unfolding fvarsOf_def by (simp add: map_pair_def)+
 
 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
 
diff -r e716209814b3 -r ba31032887db src/HOL/BNF/Examples/Misc_Data.thy
--- a/src/HOL/BNF/Examples/Misc_Data.thy	Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Thu Sep 27 00:40:51 2012 +0200
@@ -21,6 +21,8 @@
 data ('b, 'c, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
+data hfset = HFset "hfset fset"
+
 data lambda =
   Var string |
   App lambda lambda |
diff -r e716209814b3 -r ba31032887db src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Sep 27 00:40:51 2012 +0200
@@ -12,21 +12,21 @@
 imports TreeFI
 begin
 
-hide_const (open) Quotient_Product.prod_rel
-hide_fact (open) Quotient_Product.prod_rel_def
-
-codata_raw stream: 's = "'a \<times> 's"
+codata 'a stream = Stream (hdd: 'a) (tll: "'a stream")
 
 (* selectors for streams *)
-definition "hdd as \<equiv> fst (stream_dtor as)"
-definition "tll as \<equiv> snd (stream_dtor as)"
+lemma hdd_def': "hdd as = fst (stream_dtor as)"
+unfolding hdd_def stream_case_def fst_def by (rule refl)
+
+lemma tll_def': "tll as = snd (stream_dtor as)"
+unfolding tll_def stream_case_def snd_def by (rule refl)
 
 lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \<odot> g) t) = f t"
-unfolding hdd_def pair_fun_def stream.dtor_unfold by simp
+unfolding hdd_def' pair_fun_def stream.dtor_unfold by simp
 
 lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \<odot> g) t) =
  stream_dtor_unfold (f \<odot> g) (g t)"
-unfolding tll_def pair_fun_def stream.dtor_unfold by simp
+unfolding tll_def' pair_fun_def stream.dtor_unfold by simp
 
 (* infinite trees: *)
 coinductive infiniteTr where
@@ -51,12 +51,10 @@
 definition "konigPath \<equiv> stream_dtor_unfold
   (lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
 
-lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t"
-unfolding konigPath_def by simp
-
-lemma tll_simps2[simp]: "tll (konigPath t) =
-  konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
-unfolding konigPath_def by simp
+lemma konigPath_simps[simp]:
+"hdd (konigPath t) = lab t"
+"tll (konigPath t) = konigPath (SOME tr. tr \<in> listF_set (sub t) \<and> infiniteTr tr)"
+unfolding konigPath_def by simp+
 
 (* proper paths in trees: *)
 coinductive properPath where
@@ -115,15 +113,9 @@
 (* some more stream theorems *)
 
 lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> tll)"
-unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def]
+unfolding stream_map_def pair_fun_def hdd_def'[abs_def] tll_def'[abs_def]
   map_pair_def o_def prod_case_beta by simp
 
-lemma prod_rel[simp]: "prod_rel \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
-unfolding prod_rel_def by auto
-
-lemmas stream_coind =
-  mp[OF stream.dtor_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def]
-
 definition plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
   [simp]: "plus xs ys =
     stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
@@ -136,22 +128,22 @@
 definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
 
 lemma "ones \<oplus> ones = twos"
-by (intro stream_coind[where P="%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
+by (rule stream.coinduct[of "%x1 x2. \<exists>x. x1 = ones \<oplus> ones \<and> x2 = twos"]) auto
 
 lemma "n \<cdot> twos = ns (2 * n)"
-by (intro stream_coind[where P="%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>n. x1 = n \<cdot> twos \<and> x2 = ns (2 * n)"]) force+
 
 lemma prod_scalar: "(n * m) \<cdot> xs = n \<cdot> m \<cdot> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>n m xs. x1 = (n * m) \<cdot> xs \<and> x2 = n \<cdot> m \<cdot> xs"]) force+
 
 lemma scalar_plus: "n \<cdot> (xs \<oplus> ys) = n \<cdot> xs \<oplus> n \<cdot> ys"
-by (intro stream_coind[where P="%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
+by (rule stream.coinduct[of "%x1 x2. \<exists>n xs ys. x1 = n \<cdot> (xs \<oplus> ys) \<and> x2 = n \<cdot> xs \<oplus> n \<cdot> ys"])
    (force simp: add_mult_distrib2)+
 
 lemma plus_comm: "xs \<oplus> ys = ys \<oplus> xs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys. x1 = xs \<oplus> ys \<and> x2 = ys \<oplus> xs"]) force+
 
 lemma plus_assoc: "(xs \<oplus> ys) \<oplus> zs = xs \<oplus> ys \<oplus> zs"
-by (intro stream_coind[where P="%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
+by (rule stream.coinduct[of "%x1 x2. \<exists>xs ys zs. x1 = (xs \<oplus> ys) \<oplus> zs \<and> x2 = xs \<oplus> ys \<oplus> zs"]) force+
 
 end
diff -r e716209814b3 -r ba31032887db src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Sep 26 19:50:10 2012 +0200
+++ b/src/HOL/ROOT	Thu Sep 27 00:40:51 2012 +0200
@@ -625,7 +625,6 @@
   description {* Examples for Bounded Natural Functors *}
   options [document = false]
   theories
-    HFset
     Lambda_Term
     Process
     TreeFsetI