# HG changeset patch
# User paulson
# Date 850729808 -3600
# Node ID 8ba800a46e14372cba02ebce903bc0352e7b2966
# Parent  46de4b035f009d5765b8ea73a3093d1e32265808
Removed a rogue TAB

diff -r 46de4b035f00 -r 8ba800a46e14 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Mon Dec 16 10:41:26 1996 +0100
+++ b/src/HOLCF/Pcpo.ML	Mon Dec 16 10:50:08 1996 +0100
@@ -36,16 +36,16 @@
 qed_goal "maxinch_is_thelub" Pcpo.thy "is_chain Y ==> \
 \       max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::pcpo))" 
 (fn prems => 
-	[
-	cut_facts_tac prems 1,
-	rtac iffI 1,
-	fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1,
-	rewtac max_in_chain_def,
-	safe_tac (HOL_cs addSIs [antisym_less]),
-	fast_tac (HOL_cs addSEs [chain_mono3]) 1,
-	dtac sym 1,
-	fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1
-	]);
+        [
+        cut_facts_tac prems 1,
+        rtac iffI 1,
+        fast_tac (HOL_cs addSIs [thelubI,lub_finch1]) 1,
+        rewtac max_in_chain_def,
+        safe_tac (HOL_cs addSIs [antisym_less]),
+        fast_tac (HOL_cs addSEs [chain_mono3]) 1,
+        dtac sym 1,
+        fast_tac ((HOL_cs addSEs [is_ub_thelub]) addss !simpset) 1
+        ]);
 
 
 (* ------------------------------------------------------------------------ *)
@@ -163,7 +163,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val eq_UU_sym = prove_goal Pcpo.thy "(UU = x) = (x = UU)" (fn _ => [
-	fast_tac HOL_cs 1]);
+        fast_tac HOL_cs 1]);
 
 qed_goal "eq_UU_iff" Pcpo.thy "(x=UU)=(x<<UU)"
  (fn prems =>