--- a/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:19 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100
@@ -128,6 +128,12 @@
end
+definition id_rep :: "'a \<Rightarrow> 'a" where "id_rep = (\<lambda>x. x)"
+definition id_abs :: "'a \<Rightarrow> 'a" where "id_abs = (\<lambda>x. x)"
+
+lemma type_definition_id_rep_abs_UNIV: "type_definition id_rep id_abs UNIV"
+ unfolding id_rep_def id_abs_def by unfold_locales auto
+
lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
@@ -137,4 +143,7 @@
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"
+hide_const id_rep id_abs
+hide_fact id_rep_def id_abs_def type_definition_id_rep_abs_UNIV
+
end