src/ZF/OrderType.thy

 (*  Title:      ZF/OrderType.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
-
 *)
 
 header{*Order Types and Ordinal Arithmetic*}
 
 theory OrderType imports OrderArith OrdQuant Nat_ZF begin

 apply (rule_tac a=x in wf_on_induct, assumption+)
 apply (simp (no_asm_simp) add: ordermap_pred_unfold)
 apply (rule OrdI [OF _ Ord_is_Transset])
 apply (unfold pred_def Transset_def)
 apply (blast intro: trans_onD
-	     dest!: ordermap_unfold [THEN equalityD1])+ 
+             dest!: ordermap_unfold [THEN equalityD1])+ 
 done
 
 lemma Ord_ordertype: 
     "well_ord(A,r) ==> Ord(ordertype(A,r))"
 apply (unfold ordertype_def)
 apply (subst image_fun [OF ordermap_type subset_refl])
 apply (rule OrdI [OF _ Ord_is_Transset])
 prefer 2 apply (blast intro: Ord_ordermap)
 apply (unfold Transset_def well_ord_def)
 apply (blast intro: trans_onD
-	     dest!: ordermap_unfold [THEN equalityD1])
+             dest!: ordermap_unfold [THEN equalityD1])
 done
 
 
 subsubsection{*ordermap preserves the orderings in both directions *}