# HG changeset patch
# User huffman
# Date 1117833395 -7200
# Node ID cfe047ad6384e1ee3333b72edc40ad234812a92d
# Parent  d67baef02f78d50aefc49e0f73a5ccf66259ba42
changed to work with new contI, contlubE, etc.; renamed strictness rules for consistency

diff -r d67baef02f78 -r cfe047ad6384 src/HOLCF/TypedefPcpo.thy
--- a/src/HOLCF/TypedefPcpo.thy	Fri Jun 03 23:15:16 2005 +0200
+++ b/src/HOLCF/TypedefPcpo.thy	Fri Jun 03 23:16:35 2005 +0200
@@ -100,7 +100,7 @@
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
 shows "cont Rep"
- apply (rule contI[rule_format])
+ apply (rule contI)
  apply (simp only: typedef_is_lub [OF type less adm, THEN thelubI])
  apply (subst type_definition.Abs_inverse [OF type])
   apply (erule lub_Rep_in_A [OF type less adm])
@@ -123,14 +123,14 @@
     and f_in_A: "\<And>x. f x \<in> A"
     and cont_f: "cont f"
 shows "cont (\<lambda>x. Abs (f x))"
- apply (rule contI[rule_format])
+ apply (rule contI)
  apply (rule is_lubI)
   apply (rule ub_rangeI)
   apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
   apply (rule monofun_fun_arg [OF cont2mono [OF cont_f]])
   apply (erule is_ub_thelub)
  apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
- apply (simp only: contlubE[rule_format, OF cont2contlub [OF cont_f]])
+ apply (simp only: contlubE [OF cont2contlub [OF cont_f]])
  apply (rule is_lub_thelub)
   apply (erule ch2ch_monofun [OF cont2mono [OF cont_f]])
  apply (rule ub_rangeI)
@@ -181,7 +181,7 @@
   subset, @{term Rep} and @{term Abs} are both strict.
 *}
 
-theorem typedef_strict_Abs:
+theorem typedef_Abs_strict:
 assumes type: "type_definition Rep Abs A"
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
@@ -190,12 +190,12 @@
  apply (simp add: type_definition.Abs_inverse [OF type UU_in_A])
 done
 
-theorem typedef_strict_Rep:
+theorem typedef_Rep_strict:
 assumes type: "type_definition Rep Abs A"
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and UU_in_A: "\<bottom> \<in> A"
 shows "Rep \<bottom> = \<bottom>"
- apply (rule typedef_strict_Abs [OF type less UU_in_A, THEN subst])
+ apply (rule typedef_Abs_strict [OF type less UU_in_A, THEN subst])
  apply (rule type_definition.Abs_inverse [OF type UU_in_A])
 done