# HG changeset patch
# User huffman
# Date 1117834641 -7200
# Node ID ea49a9c7ff7c5106de47d86dbf109e9d26dc017e
# Parent  96f0c85462651a35bf08b3a94cca8c44737f3c61
fixed some renamed theorems

diff -r 96f0c8546265 -r ea49a9c7ff7c src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Fri Jun 03 23:36:17 2005 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Fri Jun 03 23:37:21 2005 +0200
@@ -207,7 +207,7 @@
 by (rtac adm_eq 1);
 by (cont_tacR 1);
 by (rtac allI 1);
-by (stac strict_Rep_CFun1 1);
+by (stac Rep_CFun_strict1 1);
 by (rtac refl 1);
 by (Simp_tac 1);
 by (rtac allI 1);
@@ -232,7 +232,7 @@
 by (rtac adm_eq 1);
 by (cont_tacR 1);
 by (rtac allI 1);
-by (stac strict_Rep_CFun1 1);
+by (stac Rep_CFun_strict1 1);
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
@@ -261,7 +261,7 @@
 by (rtac adm_eq 1);
 by (cont_tacR 1);
 by (rtac allI 1);
-by (stac strict_Rep_CFun1 1);
+by (stac Rep_CFun_strict1 1);
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
diff -r 96f0c8546265 -r ea49a9c7ff7c src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Fri Jun 03 23:36:17 2005 +0200
+++ b/src/HOLCF/ex/Stream.thy	Fri Jun 03 23:37:21 2005 +0200
@@ -28,7 +28,7 @@
 consts
  
   i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
-  i_th :: "nat => 'a stream => 'a"        (* the i-th element ä*)
+  i_th :: "nat => 'a stream => 'a"        (* the i-th element *)
 
   sconc         :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) 
   constr_sconc  :: "'a stream => 'a stream => 'a stream" (* constructive *)
@@ -135,7 +135,7 @@
 by (rule stream.casedist [of s], auto)
 
 lemma monofun_rt_mult: "x << s ==> iterate i rt x << iterate i rt s"
-by (insert monofun_iterate2 [of i "rt"], simp add: monofun, auto)
+by (insert monofun_iterate2 [of i "rt"], simp add: monofun_def, auto)
 
 
 
@@ -955,7 +955,7 @@
 
 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
 apply (insert contlub_scons [of a])
-by (simp only: contlub)
+by (simp only: contlub_def)
 
 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> 
                         (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
@@ -978,7 +978,7 @@
 by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp);
 
 lemma monofun_sconc: "monofun (%y. x ooo y)"
-by (simp add: monofun sconc_mono)
+by (simp add: monofun_def sconc_mono)
 
 lemma cont_sconc: "cont (%y. x ooo y)"
 apply (rule  monocontlub2cont)
diff -r 96f0c8546265 -r ea49a9c7ff7c src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Fri Jun 03 23:36:17 2005 +0200
+++ b/src/HOLCF/ex/loeckx.ML	Fri Jun 03 23:37:21 2005 +0200
@@ -55,10 +55,10 @@
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
 by (rtac refl 1);
-by (rtac cont_lubcfun 1);
+by (rtac cont_lub_cfun 1);
 by (rtac chainI 1);
 by (strip_tac 1);
-by (rtac less_cfun2 1);
+by (rtac less_cfun_ext 1);
 by (stac beta_cfun 1);
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);
@@ -88,9 +88,9 @@
 
 Goal "cont Ifix";
 by (stac fix_lemma2 1);
-by (rtac cont_lubcfun 1);
+by (rtac cont_lub_cfun 1);
 by (rtac chainI 1);
-by (rtac less_cfun2 1);
+by (rtac less_cfun_ext 1);
 by (stac beta_cfun 1);
 by (rtac  cont2cont_CF1L 1);
 by (rtac cont_iterate 1);