--- 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 =>