# HG changeset patch
# User kleing
# Date 1049555018 -7200
# Node ID 717bd79b976f8a760526c0b66e974095ed46f029
# Parent  b6105462ccd3d8756f2e5a4e5c005f8ce7a8a97b
cleanup, mark old (<1994) deleted files as dead

diff -r b6105462ccd3 -r 717bd79b976f src/HOLCF/cfun1.thy
--- a/src/HOLCF/cfun1.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(*  Title: 	HOLCF/cfun1.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Definition of the type ->  of continuous functions
-
-*)
-
-Cfun1 = Cont +
-
-
-(* new type of continuous functions *)
-
-types "->" 2        (infixr 5)
-
-arities "->" :: (pcpo,pcpo)term		(* No properties for ->'s range *)
-
-consts  
-	Cfun	:: "('a => 'b)set"
-	fapp	:: "('a -> 'b)=>('a => 'b)"	("(_[_])" [11,0] 1000)
-						(* usually Rep_Cfun *)
-						(* application      *)
-
-	fabs	:: "('a => 'b)=>('a -> 'b)"	(binder "LAM " 10)
-						(* usually Abs_Cfun *)
-						(* abstraction      *)
-
-	less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
-
-rules 
-
-  Cfun_def	"Cfun == {f. contX(f)}"
-
-  (*faking a type definition... *)
-  (* -> is isomorphic to Cfun   *)
-
-  Rep_Cfun		"fapp(fo):Cfun"
-  Rep_Cfun_inverse	"fabs(fapp(fo)) = fo"
-  Abs_Cfun_inverse	"f:Cfun ==> fapp(fabs(f))=f"
-
-  (*defining the abstract constants*)
-  less_cfun_def		"less_cfun(fo1,fo2) == ( fapp(fo1) << fapp(fo2) )"
-
-end
diff -r b6105462ccd3 -r 717bd79b976f src/HOLCF/cfun2.ML
--- a/src/HOLCF/cfun2.ML	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,276 +0,0 @@
-(*  Title: 	HOLCF/cfun2.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Lemmas for cfun2.thy 
-*)
-
-open Cfun2;
-
-(* ------------------------------------------------------------------------ *)
-(* access to less_cfun in class po                                          *)
-(* ------------------------------------------------------------------------ *)
-
-val less_cfun = prove_goal Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
-(fn prems =>
-	[
-	(rtac (inst_cfun_po RS ssubst) 1),
-	(fold_goals_tac [less_cfun_def]),
-	(rtac refl 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* Type 'a ->'b  is pointed                                                 *)
-(* ------------------------------------------------------------------------ *)
-
-val minimal_cfun = prove_goalw Cfun2.thy [UU_cfun_def] "UU_cfun << f"
-(fn prems =>
-	[
-	(rtac (less_cfun RS ssubst) 1),
-	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
-	(rtac contX_const 1),
-	(fold_goals_tac [UU_fun_def]),
-	(rtac minimal_fun 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* fapp yields continuous functions in 'a => 'b                             *)
-(* this is continuity of fapp in its 'second' argument                      *)
-(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_fapp2 = prove_goal Cfun2.thy "contX(fapp(fo))"
-(fn prems =>
-	[
-	(res_inst_tac [("P","contX")] CollectD 1),
-	(fold_goals_tac [Cfun_def]),
-	(rtac Rep_Cfun 1)
-	]);
-
-val monofun_fapp2 = contX_fapp2 RS contX2mono;
-(* monofun(fapp(?fo1)) *)
-
-
-val contlub_fapp2 = contX_fapp2 RS contX2contlub;
-(* contlub(fapp(?fo1)) *)
-
-(* ------------------------------------------------------------------------ *)
-(* expanded thms contX_fapp2, contlub_fapp2                                 *)
-(* looks nice with mixfix syntac _[_]                                       *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
-(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))]      *)
- 
-val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
-(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)]))   *)
-
-
-
-(* ------------------------------------------------------------------------ *)
-(* fapp is monotone in its 'first' argument                                 *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_fapp1 = prove_goalw Cfun2.thy [monofun] "monofun(fapp)"
-(fn prems =>
-	[
-	(strip_tac 1),
-	(etac (less_cfun RS subst) 1)
-	]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* monotonicity of application fapp in mixfix syntax [_]_                   *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_cfun_fun = prove_goal Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(res_inst_tac [("x","x")] spec 1),
-	(rtac (less_fun RS subst) 1),
-	(etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
-	]);
-
-
-val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
-(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1]                                    *)
-
-(* ------------------------------------------------------------------------ *)
-(* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
-(* ------------------------------------------------------------------------ *)
-
-val monofun_cfun = prove_goal Cfun2.thy
-	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac trans_less 1),
-	(etac monofun_cfun_arg 1),
-	(etac monofun_cfun_fun 1)
-	]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* ch2ch - rules for the type 'a -> 'b                                      *)
-(* use MF2 lemmas from Cont.ML                                              *)
-(* ------------------------------------------------------------------------ *)
-
-val ch2ch_fappR = prove_goal Cfun2.thy 
- "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(etac (monofun_fapp2 RS ch2ch_MF2R) 1)
-	]);
-
-
-val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
-(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x])                                 *)
-
-
-(* ------------------------------------------------------------------------ *)
-(*  the lub of a chain of continous functions is monotone                   *)
-(* use MF2 lemmas from Cont.ML                                              *)
-(* ------------------------------------------------------------------------ *)
-
-val lub_cfun_mono = prove_goal Cfun2.thy 
-	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac lub_MF2_mono 1),
-	(rtac monofun_fapp1 1),
-	(rtac (monofun_fapp2 RS allI) 1),
-	(atac 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* a lemma about the exchange of lubs for type 'a -> 'b                     *)
-(* use MF2 lemmas from Cont.ML                                              *)
-(* ------------------------------------------------------------------------ *)
-
-val ex_lubcfun = prove_goal Cfun2.thy
-	"[| is_chain(F); is_chain(Y) |] ==>\
-\		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
-\		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac ex_lubMF2 1),
-	(rtac monofun_fapp1 1),
-	(rtac (monofun_fapp2 RS allI) 1),
-	(atac 1),
-	(atac 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* the lub of a chain of cont. functions is continuous                      *)
-(* ------------------------------------------------------------------------ *)
-
-val contX_lubcfun = prove_goal Cfun2.thy 
-	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac monocontlub2contX 1),
-	(etac lub_cfun_mono 1),
-	(rtac contlubI 1),
-	(strip_tac 1),
-	(rtac (contlub_cfun_arg RS ext RS ssubst) 1),
-	(atac 1),
-	(etac ex_lubcfun 1),
-	(atac 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* type 'a -> 'b is chain complete                                          *)
-(* ------------------------------------------------------------------------ *)
-
-val lub_cfun = prove_goal Cfun2.thy 
-  "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac is_lubI 1),
-	(rtac conjI 1),
-	(rtac ub_rangeI 1),  
-	(rtac allI 1),
-	(rtac (less_cfun RS ssubst) 1),
-	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
-	(etac contX_lubcfun 1),
-	(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
-	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
-	(strip_tac 1),
-	(rtac (less_cfun RS ssubst) 1),
-	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
-	(etac contX_lubcfun 1),
-	(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
-	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
-	(etac (monofun_fapp1 RS ub2ub_monofun) 1)
-	]);
-
-val thelub_cfun = (lub_cfun RS thelubI);
-(* 
-is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
-*)
-
-val cpo_cfun = prove_goal Cfun2.thy 
-  "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
-(fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac exI 1),
-	(etac lub_cfun 1)
-	]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* Extensionality in 'a -> 'b                                               *)
-(* ------------------------------------------------------------------------ *)
-
-val ext_cfun = prove_goal Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
- (fn prems =>
-	[
-	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
-	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
-	(res_inst_tac [("f","fabs")] arg_cong 1),
-	(rtac ext 1),
-	(resolve_tac prems 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* Monotonicity of fabs                                                     *)
-(* ------------------------------------------------------------------------ *)
-
-val semi_monofun_fabs = prove_goal Cfun2.thy 
-	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
- (fn prems =>
-	[
-	(rtac (less_cfun RS iffD2) 1),
-	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
-	(resolve_tac prems 1),
-	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
-	(resolve_tac prems 1),
-	(resolve_tac prems 1)
-	]);
-
-(* ------------------------------------------------------------------------ *)
-(* Extenionality wrt. << in 'a -> 'b                                        *)
-(* ------------------------------------------------------------------------ *)
-
-val less_cfun2 = prove_goal Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
- (fn prems =>
-	[
-	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
-	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
-	(rtac semi_monofun_fabs 1),
-	(rtac contX_fapp2 1),
-	(rtac contX_fapp2 1),
-	(rtac (less_fun RS iffD2) 1),
-	(rtac allI 1),
-	(resolve_tac prems 1)
-	]);
-
-
diff -r b6105462ccd3 -r 717bd79b976f src/HOLCF/cfun2.thy
--- a/src/HOLCF/cfun2.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title: 	HOLCF/cfun2.thy
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-
-Class Instance ->::(pcpo,pcpo)po
-
-*)
-
-Cfun2 = Cfun1 + 
-
-(* Witness for the above arity axiom is cfun1.ML *)
-arities "->" :: (pcpo,pcpo)po
-
-consts	
-	UU_cfun  :: "'a->'b"
-
-rules
-
-(* instance of << for type ['a -> 'b]  *)
-
-inst_cfun_po	"(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
-
-(* definitions *)
-(* The least element in type 'a->'b *)
-
-UU_cfun_def	"UU_cfun == fabs(% x.UU)"
-
-end
-
-ML
-
-(* ----------------------------------------------------------------------*)
-(* unique setup of print translation for fapp                            *)
-(* ----------------------------------------------------------------------*)
-
-val print_translation = [("fapp",fapptr')];
-
-
diff -r b6105462ccd3 -r 717bd79b976f src/HOLCF/ex/coind.ML
--- a/src/HOLCF/ex/coind.ML	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-(*  Title: 	HOLCF/coind.ML
-    ID:         $Id$
-    Author: 	Franz Regensburger
-    Copyright   1993 Technische Universitaet Muenchen
-*)
-
-open Coind;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties                                             *)
-(* ------------------------------------------------------------------------- *)
-
-
-val nats_def2 = fix_prover Coind.thy nats_def 
-	"nats = scons[dzero][smap[dsucc][nats]]";
-
-val from_def2 = fix_prover Coind.thy from_def 
-	"from = (LAM n.scons[n][from[dsucc[n]]])";
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive  properties                                                     *)
-(* ------------------------------------------------------------------------- *)
-
-
-val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
- (fn prems =>
-	[
-	(rtac trans 1),
-	(rtac (from_def2 RS ssubst) 1),
-	(simp_tac HOLCF_ss  1),
-	(rtac refl 1)
-	]);
-
-
-val from1 = prove_goal Coind.thy "from[UU] = UU"
- (fn prems =>
-	[
-	(rtac trans 1),
-	(rtac (from RS ssubst) 1),
-	(resolve_tac  stream_constrdef 1),
-	(rtac refl 1)
-	]);
-
-val coind_rews = 
-	[iterator1, iterator2, iterator3, smap1, smap2,from1];
-
-
-(* ------------------------------------------------------------------------- *)
-(* the example                                                               *)
-(* prove:        nats = from[dzero]                                          *)
-(* ------------------------------------------------------------------------- *)
-
-
-val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
-\		 scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
- (fn prems =>
-	[
-	(res_inst_tac [("s","n")] dnat_ind 1),
-	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
-	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
-	(rtac trans 1),
-	(rtac nats_def2 1),
-	(simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
-	(rtac trans 1),
-	(etac iterator3 1),
-	(rtac trans 1),
-	(asm_simp_tac HOLCF_ss 1),
-	(rtac trans 1),
-	(etac smap2 1),
-	(rtac cfun_arg_cong 1),
-	(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
-	]);
-
-
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
- (fn prems =>
-	[
-	(res_inst_tac [("R",
-"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
-	(res_inst_tac [("x","dzero")] exI 2),
-	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
-	(rewrite_goals_tac [stream_bisim_def]),
-	(strip_tac 1),
-	(etac exE 1),
-	(res_inst_tac [("Q","n=UU")] classical2 1),
-	(rtac disjI1 1),
-	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
-	(rtac disjI2 1),
-	(etac conjE 1),
-	(hyp_subst_tac 1),
-	(hyp_subst_tac 1),
-	(res_inst_tac [("x","n")] exI 1),
-	(res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
-	(res_inst_tac [("x","from[dsucc[n]]")] exI 1),
-	(etac conjI 1),
-	(rtac conjI 1),
-	(rtac coind_lemma1 1),
-	(rtac conjI 1),
-	(rtac from 1),
-	(res_inst_tac [("x","dsucc[n]")] exI 1),
-	(fast_tac HOL_cs 1)
-	]);
-
-(* another proof using stream_coind_lemma2 *)
-
-val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
- (fn prems =>
-	[
-	(res_inst_tac [("R","% p q.? n. p = \
-\	iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
-	(rtac stream_coind_lemma2 1),
-	(strip_tac 1),
-	(etac exE 1),
-	(res_inst_tac [("Q","n=UU")] classical2 1),
-	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
-	(res_inst_tac [("x","UU::dnat")] exI 1),
-	(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
-	(etac conjE 1),
-	(hyp_subst_tac 1),
-	(hyp_subst_tac 1),
-	(rtac conjI 1),
-	(rtac (coind_lemma1 RS ssubst) 1),
-	(rtac (from RS ssubst) 1),
-	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
-	(res_inst_tac [("x","dsucc[n]")] exI 1),
-	(rtac conjI 1),
-	(rtac trans 1),
-	(rtac (coind_lemma1 RS ssubst) 1),
-	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
-	(rtac refl 1),
-	(rtac trans 1),
-	(rtac (from RS ssubst) 1),
-	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
-	(rtac refl 1),
-	(res_inst_tac [("x","dzero")] exI 1),
-	(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
-	]);
-
diff -r b6105462ccd3 -r 717bd79b976f src/LCF/lcf.ML
--- a/src/LCF/lcf.ML	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-(*  Title: 	LCF/lcf.ML
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1992  University of Cambridge
-
-For lcf.thy.  Basic lemmas about LCF
-*)
-
-open LCF;
-
-signature LCF_LEMMAS =
-sig
-  val ap_term: thm
-  val ap_thm: thm
-  val COND_cases: thm
-  val COND_cases_iff: thm
-  val Contrapos: thm
-  val cong: thm
-  val ext: thm
-  val eq_imp_less1: thm
-  val eq_imp_less2: thm
-  val less_anti_sym: thm
-  val less_ap_term: thm
-  val less_ap_thm: thm
-  val less_refl: thm
-  val less_UU: thm
-  val not_UU_eq_TT: thm
-  val not_UU_eq_FF: thm
-  val not_TT_eq_UU: thm
-  val not_TT_eq_FF: thm
-  val not_FF_eq_UU: thm
-  val not_FF_eq_TT: thm
-  val rstac: thm list -> int -> tactic
-  val stac: thm -> int -> tactic
-  val sstac: thm list -> int -> tactic
-  val strip_tac: int -> tactic
-  val tr_induct: thm
-  val UU_abs: thm
-  val UU_app: thm
-end;
-
-
-structure LCF_Lemmas : LCF_LEMMAS =
-
-struct
-
-(* Standard abbreviations *)
-
-val rstac = resolve_tac;
-fun stac th = rtac(th RS sym RS subst);
-fun sstac ths = EVERY' (map stac ths);
-
-fun strip_tac i = REPEAT(rstac [impI,allI] i); 
-
-val eq_imp_less1 = prove_goal thy "x=y ==> x << y"
-	(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]);
-
-val eq_imp_less2 = prove_goal thy "x=y ==> y << x"
-	(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]);
-
-val less_refl = refl RS eq_imp_less1;
-
-val less_anti_sym = prove_goal thy "[| x << y; y << x |] ==> x=y"
-	(fn prems => [rewrite_goals_tac[eq_def],
-		      REPEAT(rstac(conjI::prems)1)]);
-
-val ext = prove_goal thy
-	"(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))"
-	(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
-				    prem RS eq_imp_less1,
-				    prem RS eq_imp_less2]1)]);
-
-val cong = prove_goal thy "[| f=g; x=y |] ==> f(x)=g(y)"
-	(fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1,
-		      rtac refl 1]);
-
-val less_ap_term = less_refl RS mono;
-val less_ap_thm = less_refl RSN (2,mono);
-val ap_term = refl RS cong;
-val ap_thm = refl RSN (2,cong);
-
-val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"
-	(fn _ => [rtac less_anti_sym 1, rtac minimal 2,
-		  rtac less_ext 1, rtac allI 1, rtac minimal 1]);
-
-val UU_app = UU_abs RS sym RS ap_thm;
-
-val less_UU = prove_goal thy "x << UU ==> x=UU"
-	(fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
-
-
-val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)"
-	(fn prems => [rtac allI 1, rtac mp 1,
-		      res_inst_tac[("p","b")]tr_cases 2,
-		      fast_tac (FOL_cs addIs prems) 1]);
-
-
-val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)"
-	(fn prems => [rtac notI 1, rtac notE 1, rstac prems 1,
-		      rstac prems 1, atac 1]);
-
-val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos;
-val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos;
-
-val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2;
-val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2;
-val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1;
-val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1;
-val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1;
-val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1;
-
-
-val COND_cases_iff = (prove_goal thy
-  "ALL b. P(b=>x|y) <-> (b=UU-->P(UU)) & (b=TT-->P(x)) & (b=FF-->P(y))"
-	(fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU,
-				 not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1,
-		  rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2,
-		  stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)]))  RS spec;
-
-val lemma = prove_goal thy "A<->B ==> B ==> A"
-	(fn prems => [cut_facts_tac prems 1, rewrite_goals_tac [iff_def],
-		      fast_tac FOL_cs 1]);
-
-val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma));
-
-end;
-
-open LCF_Lemmas;
-
diff -r b6105462ccd3 -r 717bd79b976f src/LCF/lcf.thy
--- a/src/LCF/lcf.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-(*  Title: 	LCF/lcf.thy
-    ID:         $Id$
-    Author: 	Tobias Nipkow
-    Copyright   1992  University of Cambridge
-
-Natural Deduction Rules for LCF
-*)
-
-LCF = FOL +
-
-classes cpo < term
-
-default cpo
-
-types
- tr
- void
- ('a,'b) "*"		(infixl 6)
- ('a,'b) "+"		(infixl 5)
-
-arities
- fun, "*", "+" :: (cpo,cpo)cpo
- tr,void       :: cpo
-
-consts
- UU	:: "'a"
- TT,FF	:: "tr"
- FIX	:: "('a => 'a) => 'a"
- FST	:: "'a*'b => 'a"
- SND	:: "'a*'b => 'b"
- INL    :: "'a => 'a+'b"
- INR    :: "'b => 'a+'b"
- WHEN   :: "['a=>'c, 'b=>'c, 'a+'b] => 'c"
- adm	:: "('a => o) => o"
- VOID	:: "void"		("()")
- PAIR	:: "['a,'b] => 'a*'b"	("(1<_,/_>)" [0,0] 100)
- COND	:: "[tr,'a,'a] => 'a"	("(_ =>/ (_ |/ _))" [60,60,60] 60)
- "<<"	:: "['a,'a] => o"	(infixl 50)
-rules
-  (** DOMAIN THEORY **)
-
-  eq_def	"x=y == x << y & y << x"
-
-  less_trans	"[| x << y; y << z |] ==> x << z"
-
-  less_ext	"(ALL x. f(x) << g(x)) ==> f << g"
-
-  mono		"[| f << g; x << y |] ==> f(x) << g(y)"
-
-  minimal	"UU << x"
-
-  FIX_eq	"f(FIX(f)) = FIX(f)"
-
-  (** TR **)
-
-  tr_cases	"p=UU | p=TT | p=FF"
-
-  not_TT_less_FF "~ TT << FF"
-  not_FF_less_TT "~ FF << TT"
-  not_TT_less_UU "~ TT << UU"
-  not_FF_less_UU "~ FF << UU"
-
-  COND_UU	"UU => x | y  =  UU"
-  COND_TT	"TT => x | y  =  x"
-  COND_FF	"FF => x | y  =  y"
-
-  (** PAIRS **)
-
-  surj_pairing	"<FST(z),SND(z)> = z"
-
-  FST	"FST(<x,y>) = x"
-  SND	"SND(<x,y>) = y"
-
-  (*** STRICT SUM ***)
-
-  INL_DEF "~x=UU ==> ~INL(x)=UU"
-  INR_DEF "~x=UU ==> ~INR(x)=UU"
-
-  INL_STRICT "INL(UU) = UU"
-  INR_STRICT "INR(UU) = UU"
-
-  WHEN_UU  "WHEN(f,g,UU) = UU"
-  WHEN_INL "~x=UU ==> WHEN(f,g,INL(x)) = f(x)"
-  WHEN_INR "~x=UU ==> WHEN(f,g,INR(x)) = g(x)"
-
-  SUM_EXHAUSTION
-    "z = UU | (EX x. ~x=UU & z = INL(x)) | (EX y. ~y=UU & z = INR(y))"
-
-  (** VOID **)
-
-  void_cases	"(x::void) = UU"
-
-  (** INDUCTION **)
-
-  induct	"[| adm(P); P(UU); ALL x. P(x) --> P(f(x)) |] ==> P(FIX(f))"
-
-  (** Admissibility / Chain Completeness **)
-  (* All rules can be found on pages 199--200 of Larry's LCF book.
-     Note that "easiness" of types is not taken into account
-     because it cannot be expressed schematically; flatness could be. *)
-
-  adm_less	"adm(%x.t(x) << u(x))"
-  adm_not_less	"adm(%x.~ t(x) << u)"
-  adm_not_free  "adm(%x.A)"
-  adm_subst	"adm(P) ==> adm(%x.P(t(x)))"
-  adm_conj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
-  adm_disj	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
-  adm_imp	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
-  adm_all	"(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
-end
diff -r b6105462ccd3 -r 717bd79b976f src/LK/ex/hard-quant.ML
--- a/src/LK/ex/hard-quant.ML	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,277 +0,0 @@
-(*  Title: 	LK/ex/hard-quant
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Hard examples with quantifiers.  Can be read to test the LK system.
-From  F. J. Pelletier,
-  Seventy-Five Problems for Testing Automatic Theorem Provers,
-  J. Automated Reasoning 2 (1986), 191-216.
-  Errata, JAR 4 (1988), 236-236.
-
-Uses pc_tac rather than fast_tac when the former is significantly faster.
-*)
-
-writeln"File LK/ex/hard-quant.";
-
-goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
-by (fast_tac LK_pack 1);
-result(); 
-
-goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
-by (fast_tac LK_pack 1);
-result(); 
-
-goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
-by (fast_tac LK_pack 1);
-result(); 
-
-goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
-by (fast_tac LK_pack 1);
-result(); 
-
-writeln"Problems requiring quantifier duplication";
-
-(*Not provable by fast_tac LK_pack: needs multiple instantiation of ALL*)
-goal LK.thy "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
-by (best_tac LK_dup_pack 1);
-result();
-
-(*Needs double instantiation of the quantifier*)
-goal LK.thy "|- EX x. P(x) --> P(a) & P(b)";
-by (fast_tac LK_dup_pack 1);
-result();
-
-goal LK.thy "|- EX z. P(z) --> (ALL x. P(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Hard examples with quantifiers";
-
-writeln"Problem 18";
-goal LK.thy "|- EX y. ALL x. P(y)-->P(x)";
-by (best_tac LK_dup_pack 1);
-result(); 
-
-writeln"Problem 19";
-goal LK.thy "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 20";
-goal LK.thy "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
-\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
-by (fast_tac LK_pack 1); 
-result();
-
-writeln"Problem 21";
-goal LK.thy "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 22";
-goal LK.thy "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
-by (fast_tac LK_pack 1); 
-result();
-
-writeln"Problem 23";
-goal LK.thy "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
-by (best_tac LK_pack 1);  
-result();
-
-writeln"Problem 24";
-goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
-\   --> (EX x. P(x)&R(x))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 25";
-goal LK.thy "|- (EX x. P(x)) &  \
-\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
-\       (ALL x. P(x) --> (M(x) & L(x))) &   \
-\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
-\   --> (EX x. Q(x)&P(x))";
-by (best_tac LK_pack 1);  
-result();
-
-writeln"Problem 26";
-goal LK.thy "|- ((EX x. p(x)) <-> (EX x. q(x))) &	\
-\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
-\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
-by (pc_tac LK_pack 1);
-result();
-
-writeln"Problem 27";
-goal LK.thy "|- (EX x. P(x) & ~Q(x)) &   \
-\             (ALL x. P(x) --> R(x)) &   \
-\             (ALL x. M(x) & L(x) --> P(x)) &   \
-\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
-\         --> (ALL x. M(x) --> ~L(x))";
-by (pc_tac LK_pack 1); 
-result();
-
-writeln"Problem 28.  AMENDED";
-goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
-\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
-\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
-\   --> (ALL x. P(x) & L(x) --> M(x))";
-by (pc_tac LK_pack 1);  
-result();
-
-writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
-goal LK.thy "|- (EX x. P(x)) & (EX y. Q(y))  \
-\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
-\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
-by (pc_tac LK_pack 1); 
-result();
-
-writeln"Problem 30";
-goal LK.thy "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
-\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
-\   --> (ALL x. S(x))";
-by (fast_tac LK_pack 1);  
-result();
-
-writeln"Problem 31";
-goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \
-\       (EX x. L(x) & P(x)) & \
-\       (ALL x. ~ R(x) --> M(x))  \
-\   --> (EX x. L(x) & M(x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 32";
-goal LK.thy "|- (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
-\       (ALL x. S(x) & R(x) --> L(x)) & \
-\       (ALL x. M(x) --> R(x))  \
-\   --> (ALL x. P(x) & M(x) --> L(x))";
-by (best_tac LK_pack 1);
-result();
-
-writeln"Problem 33";
-goal LK.thy "|- (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
-\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 34  AMENDED (TWICE!!)  NOT PROVED AUTOMATICALLY";
-(*Andrews's challenge*)
-goal LK.thy "|- ((EX x. ALL y. p(x) <-> p(y))  <->		\
-\              ((EX x. q(x)) <-> (ALL y. p(y))))     <->	\
-\             ((EX x. ALL y. q(x) <-> q(y))  <->		\
-\              ((EX x. p(x)) <-> (ALL y. q(y))))";
-by (safe_goal_tac LK_pack 1);   (*53 secs*) (*13 secs*)
-by (TRYALL (fast_tac LK_pack));	(*165 secs*)  (*117 secs*)  (*138 secs*)
-(*for some reason, pc_tac leaves 14 subgoals instead of 6*)
-by (TRYALL (best_tac LK_dup_pack)); (*55 secs*) (*29 secs*) (*54 secs*)
-result();
-
-
-writeln"Problem 35";
-goal LK.thy "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))";
-by (best_tac LK_dup_pack 1);  (*27 secs??*)
-result();
-
-writeln"Problem 36";
-goal LK.thy "|- (ALL x. EX y. J(x,y)) & \
-\       (ALL x. EX y. G(x,y)) & \
-\       (ALL x y. J(x,y) | G(x,y) -->	\
-\       (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
-\   --> (ALL x. EX y. H(x,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 37";
-goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
-\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
-\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
-\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
-\   --> (ALL x. EX y. R(x,y))";
-by (pc_tac LK_pack 1);  (*slow*)
-by flexflex_tac;
-result();
-
-writeln"Problem 38. NOT PROVED";
-goal LK.thy
- "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->	\
-\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->		\
-\    (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &	\
-\            (~p(a) | ~(EX y. p(y) & r(x,y)) |				\
-\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
-
-writeln"Problem 39";
-goal LK.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 40.  AMENDED";
-goal LK.thy "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
-\                    ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 41";
-goal LK.thy "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))	\
-\         --> ~ (EX z. ALL x. f(x,z))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 42";
-goal LK.thy "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
-
-writeln"Problem 43  NOT PROVED AUTOMATICALLY";
-goal LK.thy "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y))) \
-\         --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))";
-
-writeln"Problem 44";
-goal LK.thy "|- (ALL x. f(x) -->					\
-\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &   	\
-\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))			\
-\             --> (EX x. j(x) & ~f(x))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 45";
-goal LK.thy "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))	\
-\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &	\
-\     ~ (EX y. l(y) & k(y)) &					\
-\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))			\
-\                  & (ALL y. g(y) & h(x,y) --> j(x,y)))		\
-\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
-by (best_tac LK_pack 1); 
-result();
-
-
-writeln"Problem 50";  
-goal LK.thy
-    "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 57";
-goal LK.thy
-    "|- P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
-\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Problem 59";
-(*Unification works poorly here -- the abstraction %sobj prevents efficient
-  operation of the occurs check*)
-Unify.trace_bound := !Unify.search_bound - 1; 
-goal LK.thy "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
-by (best_tac LK_dup_pack 1);
-result();
-
-writeln"Problem 60";
-goal LK.thy
-    "|- ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
-by (fast_tac LK_pack 1);
-result();
-
-writeln"Reached end of file.";
-
-(*18 June 92: loaded in 372 secs*)
-(*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
-(*29 June 92: loaded in 370 secs*)
diff -r b6105462ccd3 -r 717bd79b976f src/LK/lk.ML
--- a/src/LK/lk.ML	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-(*  Title: 	LK/lk.ML
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Tactics and lemmas for lk.thy (thanks also to Philippe de Groote)  
-*)
-
-open LK;
-
-(*Higher precedence than := facilitates use of references*)
-infix 4 add_safes add_unsafes;
-
-signature LK_RESOLVE = 
-  sig
-  datatype pack = Pack of thm list * thm list
-  val add_safes:   pack * thm list -> pack
-  val add_unsafes: pack * thm list -> pack
-  val allL_thin: thm
-  val best_tac: pack -> int -> tactic
-  val could_res: term * term -> bool
-  val could_resolve_seq: term * term -> bool
-  val cutL_tac: string -> int -> tactic
-  val cutR_tac: string -> int -> tactic
-  val conL: thm
-  val conR: thm
-  val empty_pack: pack
-  val exR_thin: thm
-  val fast_tac: pack -> int -> tactic
-  val filseq_resolve_tac: thm list -> int -> int -> tactic
-  val forms_of_seq: term -> term list
-  val has_prems: int -> thm -> bool   
-  val iffL: thm
-  val iffR: thm
-  val less: thm * thm -> bool
-  val LK_dup_pack: pack
-  val LK_pack: pack
-  val pc_tac: pack -> int -> tactic
-  val prop_pack: pack
-  val repeat_goal_tac: pack -> int -> tactic
-  val reresolve_tac: thm list -> int -> tactic   
-  val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic   
-  val safe_goal_tac: pack -> int -> tactic
-  val step_tac: pack -> int -> tactic
-  val symL: thm
-  val TrueR: thm
-  end;
-
-
-structure LK_Resolve : LK_RESOLVE = 
-struct
-
-(*Cut and thin, replacing the right-side formula*)
-fun cutR_tac (sP: string) i = 
-    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
-
-(*Cut and thin, replacing the left-side formula*)
-fun cutL_tac (sP: string) i = 
-    res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinL (i+1);
-
-
-(** If-and-only-if rules **)
-val iffR = prove_goalw LK.thy [iff_def]
-    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
-
-val iffL = prove_goalw LK.thy [iff_def]
-   "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
- (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
-
-val TrueR = prove_goalw LK.thy [True_def]
-    "$H |- $E, True, $F"
- (fn _=> [ rtac impR 1, rtac basic 1 ]);
-
-
-(** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
-
-val allL_thin = prove_goal LK.thy 
-    "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
- (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
-
-val exR_thin = prove_goal LK.thy 
-    "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
- (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
-
-(* Symmetry of equality in hypotheses *)
-val symL = prove_goal LK.thy 
-    "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
- (fn prems=>
-  [ (rtac cut 1),
-    (rtac thinL 2),
-    (resolve_tac prems 2),
-    (resolve_tac [basic RS sym] 1) ]);
-
-
-(**** Theorem Packs ****)
-
-datatype pack = Pack of thm list * thm list;
-
-(*A theorem pack has the form  (safe rules, unsafe rules)
-  An unsafe rule is incomplete or introduces variables in subgoals,
-  and is tried only when the safe rules are not applicable.  *)
-
-fun less (rl1,rl2) = (nprems_of rl1) < (nprems_of rl2);
-
-val empty_pack = Pack([],[]);
-
-fun (Pack(safes,unsafes)) add_safes ths   = 
-    Pack(sort less (ths@safes), unsafes);
-
-fun (Pack(safes,unsafes)) add_unsafes ths = 
-    Pack(safes, sort less (ths@unsafes));
-
-(*The rules of LK*)
-val prop_pack = empty_pack add_safes 
-	        [basic, refl, conjL, conjR, disjL, disjR, impL, impR, 
-		 notL, notR, iffL, iffR];
-
-val LK_pack = prop_pack add_safes   [allR, exL] 
-			add_unsafes [allL_thin, exR_thin];
-
-val LK_dup_pack = prop_pack add_safes   [allR, exL] 
-			    add_unsafes [allL, exR];
-
-
-
-(*Returns the list of all formulas in the sequent*)
-fun forms_of_seq (Const("Seqof",_) $ P $ u) = P :: forms_of_seq u
-  | forms_of_seq (H $ u) = forms_of_seq u
-  | forms_of_seq _ = [];
-
-(*Tests whether two sequences (left or right sides) could be resolved.
-  seqp is a premise (subgoal), seqc is a conclusion of an object-rule.
-  Assumes each formula in seqc is surrounded by sequence variables
-  -- checks that each concl formula looks like some subgoal formula.
-  It SHOULD check order as well, using recursion rather than forall/exists*)
-fun could_res (seqp,seqc) =
-      forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc)) 
-                              (forms_of_seq seqp))
-             (forms_of_seq seqc);
-
-(*Tests whether two sequents G|-H could be resolved, comparing each side.*)
-fun could_resolve_seq (prem,conc) =
-  case (prem,conc) of
-      (_ $ Abs(_,_,leftp) $ Abs(_,_,rightp),
-       _ $ Abs(_,_,leftc) $ Abs(_,_,rightc)) =>
-	  could_res (leftp,leftc)  andalso  could_res (rightp,rightc)
-    | _ => false;
-
-
-(*Like filt_resolve_tac, using could_resolve_seq
-  Much faster than resolve_tac when there are many rules.
-  Resolve subgoal i using the rules, unless more than maxr are compatible. *)
-fun filseq_resolve_tac rules maxr = SUBGOAL(fn (prem,i) =>
-  let val rls = filter_thms could_resolve_seq (maxr+1, prem, rules)
-  in  if length rls > maxr  then  no_tac  else resolve_tac rls i
-  end);
-
-
-(*Predicate: does the rule have n premises? *)
-fun has_prems n rule =  (nprems_of rule = n);
-
-(*Continuation-style tactical for resolution.
-  The list of rules is partitioned into 0, 1, 2 premises.
-  The resulting tactic, gtac, tries to resolve with rules.
-  If successful, it recursively applies nextac to the new subgoals only.
-  Else fails.  (Treatment of goals due to Ph. de Groote) 
-  Bind (RESOLVE_THEN rules) to a variable: it preprocesses the rules. *)
-
-(*Takes rule lists separated in to 0, 1, 2, >2 premises.
-  The abstraction over state prevents needless divergence in recursion.
-  The 9999 should be a parameter, to delay treatment of flexible goals. *)
-fun RESOLVE_THEN rules =
-  let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
-      fun tac nextac i = STATE (fn state =>  
-	  filseq_resolve_tac rls0 9999 i 
-	  ORELSE
-	  (DETERM(filseq_resolve_tac rls1 9999 i) THEN  TRY(nextac i))
-	  ORELSE
-	  (DETERM(filseq_resolve_tac rls2 9999 i) THEN  TRY(nextac(i+1))
-					THEN  TRY(nextac i)) )
-  in  tac  end;
-
-
-(*repeated resolution applied to the designated goal*)
-fun reresolve_tac rules = 
-  let val restac = RESOLVE_THEN rules;  (*preprocessing done now*)
-      fun gtac i = restac gtac i
-  in  gtac  end; 
-
-(*tries the safe rules repeatedly before the unsafe rules. *)
-fun repeat_goal_tac (Pack(safes,unsafes)) = 
-  let val restac  =    RESOLVE_THEN safes
-      and lastrestac = RESOLVE_THEN unsafes;
-      fun gtac i = restac gtac i  ORELSE  lastrestac gtac i
-  in  gtac  end; 
-
-
-(*Tries safe rules only*)
-fun safe_goal_tac (Pack(safes,unsafes)) = reresolve_tac safes;
-
-(*Tries a safe rule or else a unsafe rule.  Single-step for tracing. *)
-fun step_tac (thm_pack as Pack(safes,unsafes)) =
-    safe_goal_tac thm_pack  ORELSE'
-    filseq_resolve_tac unsafes 9999;
-
-
-(* Tactic for reducing a goal, using Predicate Calculus rules.
-   A decision procedure for Propositional Calculus, it is incomplete
-   for Predicate-Calculus because of allL_thin and exR_thin.  
-   Fails if it can do nothing.      *)
-fun pc_tac thm_pack = SELECT_GOAL (DEPTH_SOLVE (repeat_goal_tac thm_pack 1));
-
-(*The following two tactics are analogous to those provided by 
-  Provers/classical.  In fact, pc_tac is usually FASTER than fast_tac!*)
-fun fast_tac thm_pack =
-  SELECT_GOAL (DEPTH_SOLVE (step_tac thm_pack 1));
-
-fun best_tac thm_pack  = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) 
-	       (step_tac thm_pack 1));
-
-(** Contraction.  Useful since some rules are not complete. **)
-
-val conR = prove_goal LK.thy 
-    "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
- (fn prems=>
-  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-val conL = prove_goal LK.thy 
-    "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
- (fn prems=>
-  [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-end;
-
-open LK_Resolve;
diff -r b6105462ccd3 -r 717bd79b976f src/LK/lk.thy
--- a/src/LK/lk.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(*  Title: 	LK/lk.thy
-    ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Classical First-Order Sequent Calculus
-*)
-
-LK = Pure +
-
-classes term < logic
-
-default term
-
-types
- o sequence seqobj seqcont sequ sobj
-
-arities
- o :: logic
-
-consts
- True,False	:: "o"
- "="		:: "['a,'a] => o"	(infixl 50)
- "Not"		:: "o => o"		("~ _" [40] 40)
- "&"		:: "[o,o] => o"		(infixr 35)
- "|"		:: "[o,o] => o"		(infixr 30)
- "-->","<->"	:: "[o,o] => o"		(infixr 25)
- The		:: "('a => o) => 'a"	(binder "THE " 10)
- All		:: "('a => o) => o"	(binder "ALL " 10)
- Ex		:: "('a => o) => o"	(binder "EX " 10)
-
- (*Representation of sequents*)
- Trueprop	:: "[sobj=>sobj,sobj=>sobj] => prop"
- Seqof		:: "o => sobj=>sobj"
- "@Trueprop"	:: "[sequence,sequence] => prop" ("((_)/ |- (_))" [6,6] 5)
- "@MtSeq"	:: "sequence"				("" [] 1000)
- "@NmtSeq"	:: "[seqobj,seqcont] => sequence"	("__" [] 1000)
- "@MtSeqCont"	:: "seqcont"				("" [] 1000)
- "@SeqCont"	:: "[seqobj,seqcont] => seqcont"	(",/ __" [] 1000)
- ""		:: "o => seqobj"			("_" [] 1000)
- "@SeqId"	:: "id => seqobj"			("$_" [] 1000)
- "@SeqVar"	:: "var => seqobj"			("$_")
-
-rules
-  (*Structural rules*)
-
-  basic	"$H, P, $G |- $E, P, $F"
-
-  thinR	"$H |- $E, $F ==> $H |- $E, P, $F"
-  thinL	"$H, $G |- $E ==> $H, P, $G |- $E"
-
-  cut	"[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E"
-
-  (*Propositional rules*)
-
-  conjR	"[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F"
-  conjL	"$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E"
-
-  disjR	"$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F"
-  disjL	"[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E"
-
-  impR	"$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F"
-  impL	"[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E"
-
-  notR	"$H, P |- $E, $F ==> $H |- $E, ~P, $F"
-  notL	"$H, $G |- $E, P ==> $H, ~P, $G |- $E"
-
-  FalseL "$H, False, $G |- $E"
-
-  True_def "True == False-->False"
-  iff_def  "P<->Q == (P-->Q) & (Q-->P)"
-
-  (*Quantifiers*)
-
-  allR	"(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
-  allL	"$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
-
-  exR	"$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
-  exL	"(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
-
-  (*Equality*)
-
-  refl	"$H |- $E, a=a, $F"
-  sym   "$H |- $E, a=b, $F ==> $H |- $E, b=a, $F"
-  trans "[| $H|- $E, a=b, $F;  $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F"
-
-
-  (*Descriptions*)
-
-  The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> \
-\          $H |- $E, P(THE x.P(x)), $F"
-end
-
-ML
-
-(*Abstract over "sobj" -- representation of a sequence of formulae *)
-fun abs_sobj t = Abs("sobj", Type("sobj",[]), t);
-
-(*Representation of empty sequence*)
-val Sempty =  abs_sobj (Bound 0);
-
-fun seq_obj_tr(Const("@SeqId",_)$id) = id |
-    seq_obj_tr(Const("@SeqVar",_)$id) = id |
-    seq_obj_tr(fm) = Const("Seqof",dummyT)$fm;
-
-fun seq_tr(_$obj$seq) = seq_obj_tr(obj)$seq_tr(seq) |
-    seq_tr(_) = Bound 0;
-
-fun seq_tr1(Const("@MtSeq",_)) = Sempty |
-    seq_tr1(seq) = abs_sobj(seq_tr seq);
-
-fun true_tr[s1,s2] = Const("Trueprop",dummyT)$seq_tr1 s1$seq_tr1 s2;
-
-fun seq_obj_tr'(Const("Seqof",_)$fm) = fm |
-    seq_obj_tr'(id) = Const("@SeqId",dummyT)$id;
-
-fun seq_tr'(obj$sq,C) =
-      let val sq' = case sq of
-            Bound 0 => Const("@MtSeqCont",dummyT) |
-            _ => seq_tr'(sq,Const("@SeqCont",dummyT))
-      in C $ seq_obj_tr' obj $ sq' end;
-
-fun seq_tr1'(Bound 0) = Const("@MtSeq",dummyT) |
-    seq_tr1' s = seq_tr'(s,Const("@NmtSeq",dummyT));
-
-fun true_tr'[Abs(_,_,s1),Abs(_,_,s2)] =
-      Const("@Trueprop",dummyT)$seq_tr1' s1$seq_tr1' s2;
-
-val parse_translation = [("@Trueprop",true_tr)];
-val print_translation = [("Trueprop",true_tr')];
diff -r b6105462ccd3 -r 717bd79b976f src/Modal/modal0.thy
--- a/src/Modal/modal0.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title: 	91/Modal/modal0
-    ID:         $Id$
-    Author: 	Martin Coen
-    Copyright   1991  University of Cambridge
-*)
-
-Modal0 = LK +
-
-consts
-  box		:: "o=>o"	("[]_" [50] 50)
-  dia		:: "o=>o"	("<>_" [50] 50)
-  "--<",">-<"	:: "[o,o]=>o"	(infixr 25)
-  "@Lstar"	:: "[sequence,sequence]=>prop"	("(_)|L>(_)" [6,6] 5)
-  "@Rstar"	:: "[sequence,sequence]=>prop"	("(_)|R>(_)" [6,6] 5)
-  Lstar,Rstar	:: "[sobj=>sobj,sobj=>sobj]=>prop"
-
-rules
-  (* Definitions *)
-
-  strimp_def	"P --< Q == [](P --> Q)"
-  streqv_def	"P >-< Q == (P --< Q) & (Q --< P)"
-end
-
-ML
-
-local
-
-  val Lstar = "Lstar";
-  val Rstar = "Rstar";
-  val SLstar = "@Lstar";
-  val SRstar = "@Rstar";
-
-  fun star_tr c [s1,s2] = Const(c,dummyT)$LK.seq_tr1 s1$LK.seq_tr1 s2;
-  fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] = 
-         Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' s2;
-in
-val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
-val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
-end;
diff -r b6105462ccd3 -r 717bd79b976f src/Modal/s4.thy
--- a/src/Modal/s4.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title: 	91/Modal/S4
-    ID:         $Id$
-    Author: 	Martin Coen
-    Copyright   1991  University of Cambridge
-*)
-
-S4 = Modal0 +
-rules
-(* Definition of the star operation using a set of Horn clauses *)
-(* For system S4:  gamma * == {[]P | []P : gamma}               *)
-(*                 delta * == {<>P | <>P : delta}               *)
-
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
-
-(* Rules for [] and <> *)
-
-  boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
-\           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G"
-
-  diaR     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G"
-  diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
-\           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
-end
diff -r b6105462ccd3 -r 717bd79b976f src/Modal/s43.thy
--- a/src/Modal/s43.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(*  Title: 	91/Modal/S43
-    ID:         $Id$
-    Author: 	Martin Coen
-    Copyright   1991  University of Cambridge
-
-This implements Rajeev Gore's sequent calculus for S43.
-*)
-
-S43 = Modal0 +
-
-consts
-  S43pi	:: "[sobj=>sobj, sobj=>sobj, sobj=>sobj,\
-\	     sobj=>sobj, sobj=>sobj, sobj=>sobj] => prop"
-  "@S43pi" :: "[sequence, sequence, sequence, sequence, sequence,\
-\		sequence] => prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
-
-rules
-(* Definition of the star operation using a set of Horn clauses  *)
-(* For system S43: gamma * == {[]P | []P : gamma}                *)
-(*                 delta * == {<>P | <>P : delta}                *)
-
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
-
-(* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
-(* ie                                                                        *)
-(*           S1...Sk,Sk+1...Sk+m                                             *)
-(*     ----------------------------------                                    *)
-(*     <>P1...<>Pk, $G |- $H, []Q1...[]Qm                                    *)
-(*                                                                           *)
-(*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm    *)
-(*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
-(*    and 1<=i<=k and k<j<=k+m                                               *)
-
-  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
-  S43pi1
-   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> \
-\       S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
-  S43pi2
-   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> \
-\       S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
-
-(* Rules for [] and <> for S43 *)
-
-  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
-  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
-  pi1
-   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  \
-\      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\   $L1, <>P, $L2 |- $R"
-  pi2
-   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  \
-\      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> \
-\   $L |- $R1, []P, $R2"
-end
-
-ML
-
-local
-
-  val S43pi  = "S43pi";
-  val SS43pi = "@S43pi";
-
-  val tr  = LK.seq_tr1;
-  val tr' = LK.seq_tr1';
-
-  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
-	Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
-  fun s43pi_tr'[Abs(_,_,s1),Abs(_,_,s2),Abs(_,_,s3),
-		Abs(_,_,s4),Abs(_,_,s5),Abs(_,_,s6)] =
-        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
-in
-val parse_translation = [(SS43pi,s43pi_tr)];
-val print_translation = [(S43pi,s43pi_tr')]
-end
diff -r b6105462ccd3 -r 717bd79b976f src/Modal/t.thy
--- a/src/Modal/t.thy	Sat Apr 05 16:24:20 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(*  Title: 	91/Modal/T
-    ID:         $Id$
-    Author: 	Martin Coen
-    Copyright   1991  University of Cambridge
-*)
-
-T = Modal0 +
-rules
-(* Definition of the star operation using a set of Horn clauses *)
-(* For system T:  gamma * == {P | []P : gamma}                  *)
-(*                delta * == {P | <>P : delta}                  *)
-
-  lstar0         "|L>"
-  lstar1         "$G |L> $H ==> []P, $G |L> P, $H"
-  lstar2         "$G |L> $H ==>   P, $G |L>    $H"
-  rstar0         "|R>"
-  rstar1         "$G |R> $H ==> <>P, $G |R> P, $H"
-  rstar2         "$G |R> $H ==>   P, $G |R>    $H"
-
-(* Rules for [] and <> *)
-
-  boxR
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';  \
-\               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G"
-  boxL     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G"
-  diaR     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G"
-  diaL
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';  \
-\               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
-end