# HG changeset patch
# User traytel
# Date 1382450829 -7200
# Node ID 7fba375a7e7d01ec5bd7d1e8123de01186cb7871
# Parent  7bbe8209c253b23d44cc14ee684c4297db8380e3
removed junk

diff -r 7bbe8209c253 -r 7fba375a7e7d src/HOL/BNF/Basic_BNFs.thy
--- a/src/HOL/BNF/Basic_BNFs.thy	Tue Oct 22 14:22:06 2013 +0200
+++ b/src/HOL/BNF/Basic_BNFs.thy	Tue Oct 22 16:07:09 2013 +0200
@@ -229,7 +229,7 @@
   moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
   ultimately show ?thesis using card_of_ordLeq by fast
 qed
-declare [[bnf_note_all]]
+
 bnf "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
   "fun_rel op ="
 proof
@@ -278,7 +278,5 @@
   unfolding fun_rel_def Grp_def fun_eq_iff relcompp.simps conversep.simps  subset_iff image_iff
   by auto (force, metis pair_collapse)
 qed
-term fun_wit
-print_bnfs
-find_theorems fun_wit
+
 end