src/HOLCF/Fix.ML

 	(res_inst_tac [("s","f[g[y]]"),("t","y")] subst 1),
 	(etac spec 1),
 	(etac cfun_arg_cong 1)
 	]);
 
+(* ------------------------------------------------------------------------- *)
+(* a result about functions with flat codomain                               *)
+(* ------------------------------------------------------------------------- *)
+
+val flat_codom = prove_goalw Fix.thy [flat_def]
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
+	(rtac disjI1 1),
+	(rtac UU_I 1),
+	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
+	(atac 1),
+	(rtac (minimal RS monofun_cfun_arg) 1),
+	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+	(etac disjI1 1),
+	(rtac disjI2 1),
+	(rtac allI 1),
+	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
+	(atac 1),
+	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
+	(etac allE 1),(etac allE 1),
+	(dtac mp 1),
+	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(atac 1),
+	(etac allE 1),
+	(etac allE 1),
+	(dtac mp 1),
+	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+	(etac disjE 1),
+	(contr_tac 1),
+	(atac 1)
+	]);
+
 (* ------------------------------------------------------------------------ *)
 (* admissibility of special formulae and propagation                        *)
 (* ------------------------------------------------------------------------ *)
 
 val adm_less = prove_goalw  Fix.thy [adm_def]

 	(atac 1),
 	(rtac allI 1),
 	(dtac spec 1),
 	(etac spec 1)
 	]);
+
+val adm_all2 = (allI RS adm_all);
 
 val adm_subst = prove_goal  Fix.thy  
 	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
  (fn prems =>
 	[

 	(atac 1),
 	(atac 1)
 	]);
 
 
-val adm_all2 = (allI RS adm_all);
 
 val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
 	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
 	];
 
-(* ------------------------------------------------------------------------- *)
-(* a result about functions with flat codomain                               *)
-(* ------------------------------------------------------------------------- *)
-
-val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
-	(rtac disjI1 1),
-	(rtac UU_I 1),
-	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
-	(atac 1),
-	(rtac (minimal RS monofun_cfun_arg) 1),
-	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
-	(etac disjI1 1),
-	(rtac disjI2 1),
-	(rtac allI 1),
-	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
-	(atac 1),
-	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
-	(etac allE 1),(etac allE 1),
-	(dtac mp 1),
-	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(atac 1),
-	(etac allE 1),
-	(etac allE 1),
-	(dtac mp 1),
-	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
-	(etac disjE 1),
-	(contr_tac 1),
-	(atac 1)
-	]);