Reconstruction code, now packaged to avoid name clashes
authorpaulson
Fri Apr 08 18:43:39 2005 +0200 (2005-04-08)
changeset 156845ec4d21889d6
parent 15683 196f40d3ffea
child 15685 64f76b974a8d
Reconstruction code, now packaged to avoid name clashes
src/HOL/IsaMakefile
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/myres_axioms.ML
src/HOL/Tools/ATP/recon_gandalf_base.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_prelim.ML
src/HOL/Tools/ATP/recon_reconstruct_proof.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/reconstruction.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 08 10:50:02 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 08 18:43:39 2005 +0200
     1.3 @@ -100,25 +100,25 @@
     1.4    Orderings.ML Orderings.thy Ring_and_Field.thy\
     1.5    Set.ML Set.thy SetInterval.thy \
     1.6    Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
     1.7 -  Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
     1.8 -  Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
     1.9 -  Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    1.10 -  Tools/meson.ML Tools/numeral_syntax.ML \
    1.11 -  Tools/primrec_package.ML Tools/prop_logic.ML \
    1.12 -  Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    1.13 -  Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    1.14 -  Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.15 -  Tools/split_rule.ML Tools/typedef_package.ML \
    1.16 + Tools/datatype_codegen.ML Tools/datatype_package.ML Tools/datatype_prop.ML \
    1.17 + Tools/datatype_realizer.ML Tools/datatype_rep_proofs.ML \
    1.18 + Tools/inductive_codegen.ML Tools/inductive_package.ML Tools/inductive_realizer.ML \
    1.19 + Tools/meson.ML Tools/numeral_syntax.ML \
    1.20 + Tools/primrec_package.ML Tools/prop_logic.ML \
    1.21 + Tools/recdef_package.ML Tools/recfun_codegen.ML Tools/record_package.ML \
    1.22 + Tools/reconstruction.ML Tools/refute.ML Tools/refute_isar.ML \
    1.23 + Tools/rewrite_hol_proof.ML Tools/sat_solver.ML Tools/specification_package.ML \
    1.24 + Tools/split_rule.ML Tools/typedef_package.ML \
    1.25    Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
    1.26    Wellfounded_Recursion.thy Wellfounded_Relations.thy arith_data.ML antisym_setup.ML \
    1.27    blastdata.ML cladata.ML \
    1.28 -  Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.29 -  Tools/res_axioms.ML Tools/res_types_sorts.ML \
    1.30 -  Tools/ATP/recon_prelim.ML  Tools/ATP/recon_gandalf_base.ML  Tools/ATP/recon_order_clauses.ML\
    1.31 -  Tools/ATP/recon_translate_proof.ML   Tools/ATP/recon_parse.ML   Tools/ATP/recon_reconstruct_proof.ML \
    1.32 -  Tools/ATP/recon_transfer_proof.ML  Tools/ATP/myres_axioms.ML   Tools/ATP/res_clasimpset.ML \
    1.33 -  Tools/ATP/VampireCommunication.ML  Tools/ATP/SpassCommunication.ML     Tools/ATP/modUnix.ML  \
    1.34 -  Tools/ATP/watcher.sig  Tools/ATP/watcher.ML    Tools/res_atp.ML\
    1.35 + Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\
    1.36 + Tools/res_axioms.ML Tools/res_types_sorts.ML \
    1.37 + Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\
    1.38 + Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \
    1.39 + Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \
    1.40 + Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML   Tools/ATP/modUnix.ML  \
    1.41 + Tools/ATP/watcher.sig Tools/ATP/watcher.ML   Tools/res_atp.ML\
    1.42    document/root.tex hologic.ML simpdata.ML thy_syntax.ML
    1.43  	@$(ISATOOL) usedir -b -g true $(HOL_PROOF_OBJECTS) $(OUT)/Pure HOL
    1.44  
     2.1 --- a/src/HOL/Reconstruction.thy	Fri Apr 08 10:50:02 2005 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Fri Apr 08 18:43:39 2005 +0200
     2.3 @@ -14,7 +14,6 @@
     2.4  	  "Tools/res_axioms.ML"
     2.5  	  "Tools/res_types_sorts.ML"
     2.6  
     2.7 -(*
     2.8            "Tools/ATP/recon_prelim.ML"
     2.9  	  "Tools/ATP/recon_gandalf_base.ML"
    2.10   	  "Tools/ATP/recon_order_clauses.ML"
    2.11 @@ -27,7 +26,6 @@
    2.12  	  "Tools/ATP/watcher.sig"
    2.13  	  "Tools/ATP/watcher.ML"
    2.14  	  "Tools/res_atp.ML"
    2.15 -*)
    2.16  
    2.17            "Tools/reconstruction.ML"
    2.18  
     3.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Fri Apr 08 10:50:02 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Fri Apr 08 18:43:39 2005 +0200
     3.3 @@ -32,8 +32,8 @@
     3.4  			 in 
     3.5                              if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
     3.6  			    then ( 
     3.7 -                                    let val proofextract = extract_proof (currentString^thisLine)
     3.8 -                                        val reconstr = spassString_to_reconString (currentString^thisLine) thmstring
     3.9 +                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    3.10 +                                        val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring
    3.11                                          val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    3.12                                 in
    3.13                                           TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
     4.1 --- a/src/HOL/Tools/ATP/myres_axioms.ML	Fri Apr 08 10:50:02 2005 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,444 +0,0 @@
     4.4 -(*  Author: Jia Meng, Cambridge University Computer Laboratory
     4.5 -    ID: $Id$
     4.6 -    Copyright 2004 University of Cambridge
     4.7 -
     4.8 -Transformation of axiom rules (elim/intro/etc) into CNF forms.    
     4.9 -*)
    4.10 -
    4.11 -
    4.12 -
    4.13 -
    4.14 -(* a tactic used to prove an elim-rule. *)
    4.15 -fun elimRule_tac thm =
    4.16 -    ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    4.17 -    REPEAT(Fast_tac 1);
    4.18 -
    4.19 -
    4.20 -(* This following version fails sometimes, need to investigate, do not use it now. *)
    4.21 -fun elimRule_tac' thm =
    4.22 -   ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN
    4.23 -   REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); 
    4.24 -
    4.25 -
    4.26 -exception ELIMR2FOL of string;
    4.27 -
    4.28 -(* functions used to construct a formula *)
    4.29 -
    4.30 -fun make_imp (prem,concl) = Const("op -->", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ prem $ concl;
    4.31 -
    4.32 -
    4.33 -fun make_disjs [x] = x
    4.34 -  | make_disjs (x :: xs) = Const("op |",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_disjs xs)
    4.35 -
    4.36 -
    4.37 -fun make_conjs [x] = x
    4.38 -  | make_conjs (x :: xs) = Const("op &", Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $ x $ (make_conjs xs)
    4.39 -
    4.40 -
    4.41 -fun add_EX term [] = term
    4.42 -  | add_EX term ((x,xtp)::xs) = add_EX (Const ("Ex",Type("fun",[Type("fun",[xtp,Type("bool",[])]),Type("bool",[])])) $ Abs (x,xtp,term)) xs;
    4.43 -
    4.44 -
    4.45 -exception TRUEPROP of string; 
    4.46 -
    4.47 -fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P
    4.48 -  | strip_trueprop _ = raise TRUEPROP("not a prop!");
    4.49 -
    4.50 -
    4.51 -fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P;
    4.52 -
    4.53 -
    4.54 -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q)
    4.55 -  | is_neg _ _ = false;
    4.56 -
    4.57 -
    4.58 -exception STRIP_CONCL;
    4.59 -
    4.60 -
    4.61 -fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
    4.62 -    let val P' = strip_trueprop P
    4.63 -	val prems' = P'::prems
    4.64 -    in
    4.65 -	strip_concl' prems' bvs  Q
    4.66 -    end
    4.67 -  | strip_concl' prems bvs P = 
    4.68 -    let val P' = neg (strip_trueprop P)
    4.69 -    in
    4.70 -	add_EX (make_conjs (P'::prems)) bvs
    4.71 -    end;
    4.72 -
    4.73 -
    4.74 -fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body))  = strip_concl prems ((x,xtp)::bvs) concl body
    4.75 -  | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
    4.76 -    if (is_neg P concl) then (strip_concl' prems bvs Q)
    4.77 -    else
    4.78 -	(let val P' = strip_trueprop P
    4.79 -	     val prems' = P'::prems
    4.80 -	 in
    4.81 -	     strip_concl prems' bvs  concl Q
    4.82 -	 end)
    4.83 -  | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs;
    4.84 - 
    4.85 -
    4.86 -
    4.87 -fun trans_elim (main,others,concl) =
    4.88 -    let val others' = map (strip_concl [] [] concl) others
    4.89 -	val disjs = make_disjs others'
    4.90 -    in
    4.91 -	make_imp(strip_trueprop main,disjs)
    4.92 -    end;
    4.93 -
    4.94 -
    4.95 -(* aux function of elim2Fol, take away predicate variable. *)
    4.96 -fun elimR2Fol_aux prems concl = 
    4.97 -    let val nprems = length prems
    4.98 -	val main = hd prems
    4.99 -    in
   4.100 -	if (nprems = 1) then neg (strip_trueprop main)
   4.101 -        else trans_elim (main, tl prems, concl)
   4.102 -    end;
   4.103 -
   4.104 -
   4.105 -fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; 
   4.106 -	    
   4.107 -(* convert an elim rule into an equivalent formula, of type Term.term. *)
   4.108 -fun elimR2Fol elimR = 
   4.109 -    let val elimR' = Drule.freeze_all elimR
   4.110 -	val (prems,concl) = (prems_of elimR', concl_of elimR')
   4.111 -    in
   4.112 -	case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 
   4.113 -		      => trueprop (elimR2Fol_aux prems concl)
   4.114 -                    | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl) 
   4.115 -		    | _ => raise ELIMR2FOL("Not an elimination rule!")
   4.116 -    end;
   4.117 -
   4.118 -
   4.119 -
   4.120 -(**** use prove_goalw_cterm to prove ****)
   4.121 -
   4.122 -(* convert an elim-rule into an equivalent theorem that does not have the predicate variable. *) 
   4.123 -fun transform_elim thm =
   4.124 -    let val tm = elimR2Fol thm
   4.125 -	val ctm = cterm_of (sign_of_thm thm) tm	
   4.126 -    in
   4.127 -	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac thm])
   4.128 -    end;	
   4.129 -
   4.130 -
   4.131 -
   4.132 -
   4.133 -(* some lemmas *)
   4.134 -
   4.135 -Goal "(P==True) ==> P";
   4.136 -by(Blast_tac 1);
   4.137 -qed "Eq_TrueD1";
   4.138 -
   4.139 -Goal "(P=True) ==> P";
   4.140 -by(Blast_tac 1);
   4.141 -qed "Eq_TrueD2";
   4.142 -
   4.143 -Goal "(P==False) ==> ~P";
   4.144 -by(Blast_tac 1);
   4.145 -qed "Eq_FalseD1";
   4.146 -
   4.147 -Goal "(P=False) ==> ~P";
   4.148 -by(Blast_tac 1);
   4.149 -qed "Eq_FalseD2";
   4.150 -
   4.151 -local 
   4.152 -
   4.153 -    fun prove s = prove_goal (the_context()) s (fn _ => [Simp_tac 1]);
   4.154 -
   4.155 -val small_simps = 
   4.156 -  map prove 
   4.157 -   ["(P | True) == True", "(True | P) == True",
   4.158 -    "(P & True) == P", "(True & P) == P",
   4.159 -    "(False | P) == P", "(P | False) == P",
   4.160 -    "(False & P) == False", "(P & False) == False",
   4.161 -    "~True == False", "~False == True"];
   4.162 -in
   4.163 -
   4.164 -val small_simpset = empty_ss addsimps small_simps
   4.165 -
   4.166 -end;
   4.167 -
   4.168 -
   4.169 -(* to be fixed: cnf_intro, cnf_rule, is_introR *)
   4.170 -
   4.171 -(* check if a rule is an elim rule *)
   4.172 -fun is_elimR thm = 
   4.173 -    case (concl_of thm) of (Const ("Trueprop", _) $ Var (idx,_)) => true
   4.174 -			 | Var(indx,Type("prop",[])) => true
   4.175 -			 | _ => false;
   4.176 -
   4.177 -
   4.178 -(* repeated resolution *)
   4.179 -fun repeat_RS thm1 thm2 =
   4.180 -    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
   4.181 -    in
   4.182 -	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
   4.183 -    end;
   4.184 -
   4.185 -
   4.186 -
   4.187 -(* added this function to remove True/False in a theorem that is in NNF form. *)
   4.188 -fun rm_TF_nnf thm = simplify small_simpset thm;
   4.189 -
   4.190 -
   4.191 -(* convert a theorem into NNF and also skolemize it. *)
   4.192 -fun skolem_axiom thm = 
   4.193 -    let val thm' = (skolemize o rm_TF_nnf o  make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm
   4.194 -    in 
   4.195 -	repeat_RS thm' someI_ex
   4.196 -    end;
   4.197 -
   4.198 -
   4.199 -fun isa_cls thm = make_clauses [skolem_axiom thm]
   4.200 -
   4.201 -fun cnf_elim thm = isa_cls (transform_elim thm);
   4.202 -
   4.203 -val cnf_rule = isa_cls;	
   4.204 -
   4.205 -
   4.206 -
   4.207 -(*Transfer a theorem in to theory Reconstruction.thy if it is not already
   4.208 -  inside that theory -- because it's needed for Skolemization *)
   4.209 -
   4.210 -val recon_thy = ThyInfo.get_theory"Reconstruction";
   4.211 -
   4.212 -fun transfer_to_Reconstruction thm =
   4.213 -    transfer recon_thy thm handle THM _ => thm;
   4.214 -
   4.215 -(* remove "True" clause *)
   4.216 -fun rm_redundant_cls [] = []
   4.217 -  | rm_redundant_cls (thm::thms) =
   4.218 -    let val t = prop_of thm
   4.219 -    in
   4.220 -	case t of (Const ("Trueprop", _) $ Const ("True", _)) => rm_redundant_cls thms
   4.221 -		| _ => thm::(rm_redundant_cls thms)
   4.222 -    end;
   4.223 -
   4.224 -(* transform an Isabelle thm into CNF *)
   4.225 -fun cnf_axiom thm =
   4.226 -    let val thm' = transfer_to_Reconstruction thm
   4.227 -	val thm'' = if (is_elimR thm') then (cnf_elim thm')  else cnf_rule thm'
   4.228 -    in
   4.229 -	rm_redundant_cls thm''
   4.230 -    end;
   4.231 -
   4.232 -fun meta_cnf_axiom thm = 
   4.233 -    map (zero_var_indexes o Meson.make_meta_clause) (cnf_axiom thm);
   4.234 -
   4.235 -
   4.236 -(* changed: with one extra case added *)
   4.237 -fun univ_vars_of_aux (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars
   4.238 -  | univ_vars_of_aux (Const ("Ex",_) $ Abs(_,_,body)) vars = univ_vars_of_aux body vars (* EX x. body *)
   4.239 -  | univ_vars_of_aux (P $ Q) vars =
   4.240 -    let val vars' = univ_vars_of_aux P vars
   4.241 -    in
   4.242 -	univ_vars_of_aux Q vars'
   4.243 -    end
   4.244 -  | univ_vars_of_aux (t as Var(_,_)) vars = 
   4.245 -    if (t mem vars) then vars else (t::vars)
   4.246 -  | univ_vars_of_aux _ vars = vars;
   4.247 -  
   4.248 -
   4.249 -fun univ_vars_of t = univ_vars_of_aux t [];
   4.250 -
   4.251 -
   4.252 -fun get_new_skolem epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,tp,_)))  = 
   4.253 -    let val all_vars = univ_vars_of t
   4.254 -	val sk_term = ResSkolemFunction.gen_skolem all_vars tp
   4.255 -    in
   4.256 -	(sk_term,(t,sk_term)::epss)
   4.257 -    end;
   4.258 -
   4.259 -
   4.260 -fun sk_lookup [] t = NONE
   4.261 -  | sk_lookup ((tm,sk_tm)::tms) t = if (t = tm) then SOME (sk_tm) else (sk_lookup tms t);
   4.262 -
   4.263 -
   4.264 -
   4.265 -(* get the proper skolem term to replace epsilon term *)
   4.266 -fun get_skolem epss t = 
   4.267 -    let val sk_fun = sk_lookup epss t
   4.268 -    in
   4.269 -	case sk_fun of NONE => get_new_skolem epss t
   4.270 -		     | SOME sk => (sk,epss)
   4.271 -    end;
   4.272 -
   4.273 -
   4.274 -fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t
   4.275 -  | rm_Eps_cls_aux epss (P $ Q) =
   4.276 -    let val (P',epss') = rm_Eps_cls_aux epss P
   4.277 -	val (Q',epss'') = rm_Eps_cls_aux epss' Q
   4.278 -    in
   4.279 -	(P' $ Q',epss'')
   4.280 -    end
   4.281 -  | rm_Eps_cls_aux epss t = (t,epss);
   4.282 -
   4.283 -
   4.284 -fun rm_Eps_cls epss thm =
   4.285 -    let val tm = prop_of thm
   4.286 -    in
   4.287 -	rm_Eps_cls_aux epss tm
   4.288 -    end;
   4.289 -
   4.290 -
   4.291 -(* remove the epsilon terms in a formula, by skolem terms. *)
   4.292 -fun rm_Eps _ [] = []
   4.293 -  | rm_Eps epss (thm::thms) = 
   4.294 -    let val (thm',epss') = rm_Eps_cls epss thm
   4.295 -    in
   4.296 -	thm' :: (rm_Eps epss' thms)
   4.297 -    end;
   4.298 -
   4.299 -
   4.300 -
   4.301 -(* changed, now it also finds out the name of the theorem. *)
   4.302 -(* convert a theorem into CNF and then into Clause.clause format. *)
   4.303 -fun clausify_axiom thm =
   4.304 -    let val isa_clauses = cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
   4.305 -        val isa_clauses' = rm_Eps [] isa_clauses
   4.306 -        val thm_name = Thm.name_of_thm thm
   4.307 -	val clauses_n = length isa_clauses
   4.308 -	fun make_axiom_clauses _ [] = []
   4.309 -	  | make_axiom_clauses i (cls::clss) = (ResClause.make_axiom_clause cls (thm_name,i)) :: make_axiom_clauses (i+1) clss 
   4.310 -    in
   4.311 -	make_axiom_clauses 0 isa_clauses'
   4.312 -		
   4.313 -    end;
   4.314 -  
   4.315 -
   4.316 -(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
   4.317 -
   4.318 -
   4.319 -local
   4.320 -
   4.321 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
   4.322 -	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
   4.323 -
   4.324 -
   4.325 -fun snds [] = []
   4.326 -  |   snds ((x,y)::l) = y::(snds l);
   4.327 -
   4.328 -in
   4.329 -
   4.330 -
   4.331 -fun claset_rules_of_thy thy =
   4.332 -    let val clsset = rep_cs (claset_of thy)
   4.333 -	val safeEs = #safeEs clsset
   4.334 -	val safeIs = #safeIs clsset
   4.335 -	val hazEs = #hazEs clsset
   4.336 -	val hazIs = #hazIs clsset
   4.337 -    in
   4.338 -	safeEs @ safeIs @ hazEs @ hazIs
   4.339 -    end;
   4.340 -
   4.341 -fun simpset_rules_of_thy thy =
   4.342 -    let val simpset = simpset_of thy
   4.343 -	val rules = #rules(fst (rep_ss simpset))
   4.344 -	val thms = retr_thms (snds(Net.dest rules))
   4.345 -    in
   4.346 -	thms
   4.347 -    end;
   4.348 -
   4.349 -
   4.350 -
   4.351 -(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
   4.352 -
   4.353 -(* classical rules *)
   4.354 -fun cnf_classical_rules [] err_list = ([],err_list)
   4.355 -  | cnf_classical_rules (thm::thms) err_list = 
   4.356 -    let val (ts,es) = cnf_classical_rules thms err_list
   4.357 -    in
   4.358 -	((cnf_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   4.359 -    end;
   4.360 -
   4.361 -
   4.362 -(* CNF all rules from a given theory's classical reasoner *)
   4.363 -fun cnf_classical_rules_thy thy = 
   4.364 -    let val rules = claset_rules_of_thy thy
   4.365 -    in
   4.366 -        cnf_classical_rules rules []
   4.367 -    end;
   4.368 -
   4.369 -
   4.370 -(* simplifier rules *)
   4.371 -fun cnf_simpset_rules [] err_list = ([],err_list)
   4.372 -  | cnf_simpset_rules (thm::thms) err_list =
   4.373 -    let val (ts,es) = cnf_simpset_rules thms err_list
   4.374 -    in
   4.375 -	((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   4.376 -    end;
   4.377 -
   4.378 -
   4.379 -(* CNF all simplifier rules from a given theory's simpset *)
   4.380 -fun cnf_simpset_rules_thy thy =
   4.381 -    let val thms = simpset_rules_of_thy thy
   4.382 -    in
   4.383 -	cnf_simpset_rules thms []
   4.384 -    end;
   4.385 -
   4.386 -
   4.387 -
   4.388 -(**** Convert all theorems of a classical reason/simpset into clauses (ResClause.clause) ****)
   4.389 -
   4.390 -(* classical rules *)
   4.391 -fun clausify_classical_rules [] err_list = ([],err_list)
   4.392 -  | clausify_classical_rules (thm::thms) err_list =
   4.393 -    let val (ts,es) = clausify_classical_rules thms err_list
   4.394 -    in
   4.395 -	((clausify_axiom thm)::ts,es) handle  _ => (ts,(thm::es))
   4.396 -    end;
   4.397 -
   4.398 -
   4.399 -
   4.400 -(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
   4.401 -fun clausify_classical_rules_thy thy =
   4.402 -    let val rules = claset_rules_of_thy thy
   4.403 -    in
   4.404 -	clausify_classical_rules rules []
   4.405 -    end;
   4.406 -
   4.407 -
   4.408 -(* simplifier rules *)
   4.409 -fun clausify_simpset_rules [] err_list = ([],err_list)
   4.410 -  | clausify_simpset_rules (thm::thms) err_list =
   4.411 -    let val (ts,es) = clausify_simpset_rules thms err_list
   4.412 -    in
   4.413 -	((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   4.414 -    end;
   4.415 -
   4.416 -
   4.417 -(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
   4.418 -fun clausify_simpset_rules_thy thy =
   4.419 -    let val thms = simpset_rules_of_thy thy
   4.420 -    in
   4.421 -	clausify_simpset_rules thms []
   4.422 -    end;
   4.423 -
   4.424 -(* lcp-modified code *)
   4.425 -(*
   4.426 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
   4.427 -	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
   4.428 -
   4.429 -fun snds [] = []
   4.430 -   | snds ((x,y)::l) = y::(snds l);
   4.431 -
   4.432 -fun simpset_rules_of_thy thy =
   4.433 -     let val simpset = simpset_of thy
   4.434 -	val rules = #rules(fst (rep_ss simpset))
   4.435 -	val thms = retr_thms (snds(Net.dest rules))
   4.436 -     in	thms  end;
   4.437 -
   4.438 -print_depth 200;
   4.439 -simpset_rules_of_thy Main.thy;
   4.440 -
   4.441 -
   4.442 -
   4.443 -
   4.444 -
   4.445 -*)
   4.446 -
   4.447 -end;
     5.1 --- a/src/HOL/Tools/ATP/recon_gandalf_base.ML	Fri Apr 08 10:50:02 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_gandalf_base.ML	Fri Apr 08 18:43:39 2005 +0200
     5.3 @@ -1,3 +1,6 @@
     5.4 +structure Recon_Base =
     5.5 +struct
     5.6 +
     5.7  (* Auxiliary functions *)
     5.8  
     5.9  exception Assertion of string;
    5.10 @@ -5,9 +8,6 @@
    5.11  val DEBUG = ref true;
    5.12  fun TRACE s = if !DEBUG then print s else ();
    5.13  
    5.14 -fun id x = x;
    5.15 -fun K x y = x;
    5.16 -
    5.17  exception Noassoc;
    5.18  fun assoc a [] = raise Noassoc
    5.19    | assoc a ((x, y)::t) = if a = x then y else assoc a t;
    5.20 @@ -36,3 +36,4 @@
    5.21  fun iter f a [] = a
    5.22    | iter f a (h::t) = f h (iter f a t);
    5.23  
    5.24 +end;
     6.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Fri Apr 08 10:50:02 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Fri Apr 08 18:43:39 2005 +0200
     6.3 @@ -150,25 +150,6 @@
     6.4  |   numlist n = (numlist (n - 1))@[n]
     6.5  
     6.6  
     6.7 -fun is_abs t = can dest_abs t;
     6.8 -fun is_comb t = can dest_comb t;
     6.9 -
    6.10 -fun iscomb a = if is_Free a then
    6.11 -			false
    6.12 -	      else if is_Var a then
    6.13 -			false
    6.14 -		else if is_conj a then
    6.15 -			false
    6.16 -		else if is_disj a then
    6.17 -			false
    6.18 -		else if is_forall a then
    6.19 -			false
    6.20 -		else if is_exists a then
    6.21 -			false
    6.22 -		else
    6.23 -			true;
    6.24 -
    6.25 -
    6.26  
    6.27  
    6.28  fun last(x::xs) = if xs=[] then x else last xs
    6.29 @@ -219,25 +200,6 @@
    6.30  |   numlist n = (numlist (n - 1))@[n]
    6.31  
    6.32  
    6.33 -fun is_abs t = can dest_abs t;
    6.34 -fun is_comb t = can dest_comb t;
    6.35 -
    6.36 -fun iscomb a = if is_Free a then
    6.37 -			false
    6.38 -	      else if is_Var a then
    6.39 -			false
    6.40 -		else if is_conj a then
    6.41 -			false
    6.42 -		else if is_disj a then
    6.43 -			false
    6.44 -		else if is_forall a then
    6.45 -			false
    6.46 -		else if is_exists a then
    6.47 -			false
    6.48 -		else
    6.49 -			true;
    6.50 -
    6.51 -
    6.52  
    6.53  
    6.54  fun last(x::xs) = if xs=[] then x else last xs
    6.55 @@ -250,7 +212,7 @@
    6.56  
    6.57  (* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
    6.58  
    6.59 -fun assoc3 a [] = raise Noassoc
    6.60 +fun assoc3 a [] = raise Recon_Base.Noassoc
    6.61    | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
    6.62  
    6.63  
     7.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Fri Apr 08 10:50:02 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Apr 08 18:43:39 2005 +0200
     7.3 @@ -3,6 +3,9 @@
     7.4  
     7.5  (* Auxiliary functions *)
     7.6  
     7.7 +structure Recon_Parse =
     7.8 +struct
     7.9 +
    7.10  exception ASSERTION of string;
    7.11  
    7.12  exception NOPARSE_WORD
    7.13 @@ -100,7 +103,7 @@
    7.14        fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
    7.15      
    7.16  
    7.17 -    fun kill_lines 0 = id
    7.18 +    fun kill_lines 0 = Library.I
    7.19        | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
    7.20  
    7.21      (*fun extract_proof s
    7.22 @@ -140,7 +143,7 @@
    7.23  
    7.24  
    7.25  fun several p = many (some p)
    7.26 -      fun collect (h, t) = h ^ (itlist (fn s1 => fn s2 => s1 ^ s2) t "")
    7.27 +      fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
    7.28    
    7.29        fun lower_letter s = ("a" <= s) andalso (s <= "z")
    7.30        fun upper_letter s = ("A" <= s) andalso (s <= "Z")
    7.31 @@ -464,19 +467,4 @@
    7.32                                                          (clausenum, step, P_info, newstrs)::(change_space xs) 
    7.33                                                   end
    7.34  
    7.35 -
    7.36 -
    7.37 -
    7.38 -
    7.39 -
    7.40 -(*
    7.41 -    fun gandalf_parse s =
    7.42 -      let
    7.43 -        val e = extract_proof;
    7.44 -        val t = fst(lex e)
    7.45 -        val r = parse t
    7.46 -      in
    7.47 -        r
    7.48 -      end
    7.49 -  
    7.50 -*)
    7.51 +end;
     8.1 --- a/src/HOL/Tools/ATP/recon_prelim.ML	Fri Apr 08 10:50:02 2005 +0200
     8.2 +++ b/src/HOL/Tools/ATP/recon_prelim.ML	Fri Apr 08 18:43:39 2005 +0200
     8.3 @@ -1,11 +1,3 @@
     8.4 -
     8.5 -open Goals;
     8.6 -open Unify;
     8.7 -open USyntax;
     8.8 -open Utils;
     8.9 -open Envir;
    8.10 -open Tfl;
    8.11 -open Rules;
    8.12  
    8.13  Goal "A -->A";
    8.14  by Auto_tac;
    8.15 @@ -16,37 +8,26 @@
    8.16  
    8.17  
    8.18  
    8.19 -(*val myhol = sign_of thy;*)
    8.20 -
    8.21 -val myenv = empty 0;
    8.22 -
    8.23 +val gcounter = ref 0; 
    8.24  
    8.25 -val gcounter = ref 0; 
    8.26 -      
    8.27 -exception NOMATES;
    8.28 -exception UNMATEABLE;
    8.29 -exception NOTSOME;
    8.30 -exception UNSPANNED;
    8.31  
    8.32  fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
    8.33  
    8.34  fun dest_neg(Const("Not",_) $ M) = M
    8.35    | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
    8.36  
    8.37 -fun is_abs t = can dest_abs t;
    8.38 -fun is_comb t = can dest_comb t;
    8.39  
    8.40  fun iscomb a = if is_Free a then
    8.41  			false
    8.42  	      else if is_Var a then
    8.43  			false
    8.44 -		else if is_conj a then
    8.45 +		else if USyntax.is_conj a then
    8.46  			false
    8.47 -		else if is_disj a then
    8.48 +		else if USyntax.is_disj a then
    8.49  			false
    8.50 -		else if is_forall a then
    8.51 +		else if USyntax.is_forall a then
    8.52  			false
    8.53 -		else if is_exists a then
    8.54 +		else if USyntax.is_exists a then
    8.55  			false
    8.56  		else
    8.57  			true;
    8.58 @@ -54,13 +35,6 @@
    8.59     |getstring (Free (v,T))= v;
    8.60  
    8.61  
    8.62 -fun getindexstring ((a:string),(b:int))= a;  
    8.63 -
    8.64 -fun getstrings (a,b) = let val astring = getstring a
    8.65 -                           val bstring = getstring b in
    8.66 -                           (astring,bstring)
    8.67 -                       end;
    8.68 -
    8.69  
    8.70  fun alltrue [] = true
    8.71     |alltrue (true::xs) = true andalso (alltrue xs)
    8.72 @@ -117,25 +91,25 @@
    8.73                                  false
    8.74                         end;
    8.75  
    8.76 -fun is_hol_fm f =  if is_neg f then
    8.77 -                        let val newf = dest_neg f in
    8.78 +fun is_hol_fm f =  if USyntax.is_neg f then
    8.79 +                        let val newf = USyntax.dest_neg f in
    8.80                              is_hol_fm newf
    8.81                          end
    8.82                      
    8.83 -               else if is_disj f then
    8.84 -                        let val {disj1,disj2} = dest_disj f in
    8.85 +               else if USyntax.is_disj f then
    8.86 +                        let val {disj1,disj2} = USyntax.dest_disj f in
    8.87                              (is_hol_fm disj1) andalso (is_hol_fm disj2)  (* shouldn't this be and ? *)
    8.88                          end 
    8.89 -               else if is_conj f then
    8.90 -                        let val {conj1,conj2} = dest_conj f in
    8.91 +               else if USyntax.is_conj f then
    8.92 +                        let val {conj1,conj2} = USyntax.dest_conj f in
    8.93                              (is_hol_fm conj1) andalso (is_hol_fm conj2)
    8.94                          end 
    8.95 -               else if (is_forall f) then
    8.96 -                        let val {Body, Bvar} = dest_forall f in
    8.97 +               else if (USyntax.is_forall f) then
    8.98 +                        let val {Body, Bvar} = USyntax.dest_forall f in
    8.99                              is_hol_fm Body
   8.100                          end
   8.101 -               else if (is_exists f) then
   8.102 -                        let val {Body, Bvar} = dest_exists f in
   8.103 +               else if (USyntax.is_exists f) then
   8.104 +                        let val {Body, Bvar} = USyntax.dest_exists f in
   8.105                              is_hol_fm Body
   8.106                          end
   8.107                 else if (iscomb f) then
   8.108 @@ -147,13 +121,15 @@
   8.109  d to check args *)
   8.110                 
   8.111  
   8.112 -fun hol_literal t =  (is_hol_fm t) andalso ( not ((is_conj t) orelse (is_disj t) orelse (is_forall t) orelse (is_exists t)));
   8.113 +fun hol_literal t = 
   8.114 +   (is_hol_fm t) andalso 
   8.115 +   ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t)));
   8.116  
   8.117  
   8.118  
   8.119  
   8.120  (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *)
   8.121 -fun getcombvar a = let val {Rand = rand, Rator = rator} = dest_comb a in
   8.122 +fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in
   8.123  			if (iscomb rand) then
   8.124  				getcombvar rand
   8.125  			else
   8.126 @@ -213,258 +189,12 @@
   8.127  			   snd envpair 
   8.128  			end;
   8.129  
   8.130 -fun readnewenv thisenv =let val seqlist = Seq.list_of thisenv
   8.131 -			   val envpair = hd seqlist
   8.132 -			   val env = fst envpair
   8.133 -			   val envlist = alist_of env in
   8.134 -			hd envlist
   8.135 -			end;
   8.136 -
   8.137 -
   8.138 -fun readenv thisenv = let val envlist = alist_of thisenv in
   8.139 -			
   8.140 -				hd envlist
   8.141 -			end;
   8.142 -
   8.143 -
   8.144 -
   8.145  
   8.146  
   8.147  fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]);
   8.148  
   8.149 -fun oneofthree (a,b,c) = a;
   8.150 -
   8.151 -fun twoofthree (a,b,c) = b;
   8.152 -
   8.153 -fun threeofthree (a,b,c) = c;
   8.154 -
   8.155 -val my_simps = map prover
   8.156 - [ "(x=x) = True",
   8.157 -    "(~ ~ P) = P",
   8.158 -   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
   8.159 -   
   8.160 -   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
   8.161 -   "((~P) = (~Q)) = (P=Q)" ];
   8.162 -
   8.163 -
   8.164 -(*val myss = HOL_basic_ss addsimps (my_simps@[not_all, not_ex, de_Morgan_conj, de_Morgan_disj, U_def, intersect_def, setEq_def, proposEq_def, hashset_def, subset_def]@ex_simps @ all_simps);
   8.165 -
   8.166 -*)
   8.167 -
   8.168 -(*--------------------------*)
   8.169 -(* NNF stuff from meson_tac *)
   8.170 -(*--------------------------*)
   8.171 -
   8.172 -
   8.173 -(*Prove theorems using fast_tac*)
   8.174 -fun prove_fun s = 
   8.175 -    prove_goal HOL.thy s
   8.176 -         (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
   8.177 -
   8.178 -(*------------------------------------------------------------------------*)
   8.179 -(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
   8.180 -(*------------------------------------------------------------------------*)
   8.181 -fun mygenvar ty thisenv =
   8.182 -  let val count = !gcounter
   8.183 -      val genstring = "GEN"^(string_of_int count)^"VAR" in
   8.184 -	    	gcounter := count + 1;
   8.185 -              	genvar genstring (thisenv,ty)
   8.186 -  end;  
   8.187 -
   8.188 -fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
   8.189 -			t
   8.190 -	 	
   8.191 -		else if is_forall t then
   8.192 -			let val {Body, Bvar} = dest_forall t 
   8.193 -                            val newvarenv = mygenvar(type_of Bvar) thisenv
   8.194 -                            val newvar = snd(newvarenv)
   8.195 -                            val newbod = subst_free [(Bvar,newvar)] Body
   8.196 -                            val newbod2 = renameBounds newbod thisenv in
   8.197 -                            mk_forall{Body = newbod2, Bvar = newvar}
   8.198 -                        end
   8.199 -		else if is_exists t then
   8.200 -                        let val {Body, Bvar} =dest_exists t 
   8.201 -			    val newvarenv = mygenvar(type_of Bvar) thisenv
   8.202 -                            val newvar = snd(newvarenv)
   8.203 -                            val newbod = subst_free [(Bvar,newvar)] Body
   8.204 -                            val newbod2 = renameBounds newbod thisenv in
   8.205 -                            mk_exists{Body = newbod2, Bvar = newvar}    
   8.206 -			end
   8.207 -		else if is_conj t then
   8.208 -			let val {conj1,conj2} = dest_conj t
   8.209 -			    val vpl = renameBounds conj1 thisenv
   8.210 -			    val vpr = renameBounds conj2 thisenv in
   8.211 -		            mk_conj {conj1 = vpl, conj2 = vpr}
   8.212 -			end
   8.213 -		else 
   8.214 -			let val {disj1, disj2} = dest_disj t 
   8.215 -			    val vpl = renameBounds disj1 thisenv
   8.216 -			    val  vpr = renameBounds disj2  thisenv in
   8.217 -			    mk_disj {disj1 = vpl,disj2= vpr}  
   8.218 -			end;
   8.219 -                	
   8.220 -
   8.221 -(*-----------------*)
   8.222 -(* from hologic.ml *)
   8.223 -(*-----------------*)
   8.224 -val boolT = Type ("bool", []);
   8.225 -
   8.226 -val Trueprop = Const ("Trueprop", boolT --> propT);
   8.227 -
   8.228 -fun mk_Trueprop P = Trueprop $ P;
   8.229 -
   8.230 -fun eq_const T = Const ("op =", [T, T] ---> boolT);
   8.231 -fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
   8.232 -
   8.233 -fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   8.234 - | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
   8.235  
   8.236  
   8.237 -(*-----------------------------------------------------------------------*)
   8.238 -(* Making a THM from a subgoal and other such things                     *)
   8.239 -(*-----------------------------------------------------------------------*)
   8.240 -
   8.241 -fun thmfromgoal goalnum = let val mygoal = getgoal goalnum
   8.242 -                              val  mycgoal = cterm_of Mainsign mygoal in
   8.243 -                              assume mycgoal
   8.244 -                          end;
   8.245 -
   8.246 -fun termfromgoal goalnum = let val mygoal = getgoal goalnum
   8.247 -                               val {Rand = myra, Rator = myrat} = dest_comb mygoal in
   8.248 -                               myra
   8.249 -                           end;
   8.250 -
   8.251 -fun thmfromterm t = let val propterm = mk_Trueprop t 
   8.252 -                        val mycterm = cterm_of Mainsign propterm in
   8.253 -                        assume mycterm
   8.254 -                    end;
   8.255 -
   8.256 -fun termfromthm t = let val conc = concl_of t 
   8.257 -                        val {Rand = myra, Rator = myrat} = dest_comb conc in
   8.258 -                        myra
   8.259 -                    end;
   8.260 -
   8.261 -fun goalfromterm t = let val pterm = mk_Trueprop t  
   8.262 -                         val ct = cterm_of Mainsign  pterm in
   8.263 -                         goalw_cterm [] ct
   8.264 -                     end;
   8.265 -
   8.266 -fun termfromgoalimp goalnum = let val mygoal = getgoal goalnum
   8.267 -                               val {Rand = myra1, Rator = myrat1} = dest_comb mygoal 
   8.268 -                               val  {Rand = myra, Rator = myrat} = dest_comb myra1 in
   8.269 -                               myra
   8.270 -                           end;
   8.271 -
   8.272 -
   8.273 -fun mkvars (a,b:term) = let val thetype = type_of b 
   8.274 -                           val stringa =( fst a)
   8.275 -                            val newa = Free (stringa, thetype) in
   8.276 -                            (newa,b)
   8.277 -                        end;
   8.278 -
   8.279 -fun glue [] thestring = thestring
   8.280 -  |glue (""::[]) thestring = thestring 
   8.281 -  |glue (a::[]) thestring = thestring^" "^a 
   8.282 -  |glue (a::rest) thestring = let val newstring = thestring^" "^a in
   8.283 -                                 glue rest newstring
   8.284 -                             end;
   8.285 -
   8.286 -exception STRINGEXCEP;
   8.287 - 
   8.288 -fun getvstring (Var (v,T)) = fst v
   8.289 -   |getvstring (Free (v,T))= v;
   8.290 -
   8.291 -  
   8.292 -fun getindexstring ((a:string),(b:int))= a;  
   8.293 -
   8.294 -fun getstrings (a,b) = let val astring = getstring a
   8.295 -                           val bstring = getstring b in
   8.296 -                           (astring,bstring)
   8.297 -                       end;
   8.298 -(*
   8.299 -fun getvstrings (a,b) = let val astring = getvstring a
   8.300 -                           val bstring = getvstring b in
   8.301 -                           (astring,bstring)
   8.302 -                       end;
   8.303 -*)
   8.304 - 
   8.305 -
   8.306 -
   8.307 -(*------------------------------------------------------------------------*)
   8.308 -(* Renaming all the bound vars in the term - sort of fake `Skolemisation' *)
   8.309 -(*------------------------------------------------------------------------*)
   8.310 -fun mygenvar ty thisenv =
   8.311 -  let val count = !gcounter
   8.312 -      val genstring = "GEN"^(string_of_int count)^"VAR" in
   8.313 -	    	gcounter := count + 1;
   8.314 -              	genvar genstring (thisenv,ty)
   8.315 -  end;  
   8.316 -
   8.317 -fun renameBounds t thisenv = if (is_Var t) orelse (is_Free t) orelse (iscomb t) then
   8.318 -			t
   8.319 -	 	
   8.320 -		else if is_forall t then
   8.321 -			let val {Body, Bvar} = dest_forall t 
   8.322 -                            val newvarenv = mygenvar(type_of Bvar) thisenv
   8.323 -                            val newvar = snd(newvarenv)
   8.324 -                            val newbod = subst_free [(Bvar,newvar)] Body
   8.325 -                            val newbod2 = renameBounds newbod thisenv in
   8.326 -                            mk_forall{Body = newbod2, Bvar = newvar}
   8.327 -                        end
   8.328 -		else if is_exists t then
   8.329 -                        let val {Body, Bvar} =dest_exists t 
   8.330 -			    val newvarenv = mygenvar(type_of Bvar) thisenv
   8.331 -                            val newvar = snd(newvarenv)
   8.332 -                            val newbod = subst_free [(Bvar,newvar)] Body
   8.333 -                            val newbod2 = renameBounds newbod thisenv in
   8.334 -                            mk_exists{Body = newbod2, Bvar = newvar}    
   8.335 -			end
   8.336 -		else if is_conj t then
   8.337 -			let val {conj1,conj2} = dest_conj t
   8.338 -			    val vpl = renameBounds conj1 thisenv
   8.339 -			    val vpr = renameBounds conj2 thisenv in
   8.340 -		            mk_conj {conj1 = vpl, conj2 = vpr}
   8.341 -			end
   8.342 -		else 
   8.343 -			let val {disj1, disj2} = dest_disj t 
   8.344 -			    val vpl = renameBounds disj1 thisenv
   8.345 -			    val  vpr = renameBounds disj2  thisenv in
   8.346 -			    mk_disj {disj1 = vpl,disj2= vpr}  
   8.347 -			end;
   8.348 -                	
   8.349 -
   8.350 -
   8.351 -exception VARFORM_PROBLEM;
   8.352 -		
   8.353 -fun varform t = if (hol_literal t) then
   8.354 -			t
   8.355 -	 	
   8.356 -		else if is_forall t then
   8.357 -			let val {Body, Bvar} = dest_forall t 
   8.358 -         (* need to subst schematic vars for Bvar here, e.g. x becomes ?x *)
   8.359 -                         val newB = free2var Bvar
   8.360 -                         val newBody = subst_free[(Bvar, newB)] Body in
   8.361 -			    varform newBody
   8.362 -			end
   8.363 -		else if is_exists t then
   8.364 -        (* Shouldn't really be any exists in term due to Skolemisation*)
   8.365 -			let val {Body, Bvar} =dest_exists t in
   8.366 -			    varform Body
   8.367 -			end
   8.368 -		else if is_conj t then
   8.369 -			let val {conj1,conj2} = dest_conj t
   8.370 -			    val vpl = varform conj1 
   8.371 -			    val vpr = varform conj2 in
   8.372 -		            mk_conj {conj1 = vpl, conj2 = vpr}
   8.373 -			end
   8.374 -		else if is_disj t then
   8.375 -			let val {disj1, disj2} = dest_disj t 
   8.376 -			    val vpl = varform disj1
   8.377 -			    val  vpr = varform disj2 in
   8.378 -			    mk_disj {disj1 = vpl,disj2= vpr}  
   8.379 -			end
   8.380 -                else
   8.381 -                        raise VARFORM_PROBLEM;
   8.382                  	
   8.383   
   8.384  exception ASSERTION of string;
     9.1 --- a/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Fri Apr 08 10:50:02 2005 +0200
     9.2 +++ b/src/HOL/Tools/ATP/recon_reconstruct_proof.ML	Fri Apr 08 18:43:39 2005 +0200
     9.3 @@ -53,7 +53,7 @@
     9.4                              val prems = prems_of th
     9.5                              val fac1 = get_nth (lit1+1) prems
     9.6                              val fac2 = get_nth (lit2+1) prems
     9.7 -                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
     9.8 +                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
     9.9                              val newenv = getnewenv unif_env
    9.10                              val envlist = alist_of newenv
    9.11                              
    9.12 @@ -140,7 +140,7 @@
    9.13  
    9.14                             (* get bit of th2 to unify with lhs of th1 *)
    9.15                              val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs
    9.16 -                            val unif_env = unifiers (Mainsign,myenv, [(unif_lit, lhs)])
    9.17 +                            val unif_env = unifiers (Mainsign,Envir.empty 0, [(unif_lit, lhs)])
    9.18                              val newenv = getnewenv unif_env
    9.19                              val envlist = alist_of newenv
    9.20                              val newsubsts = mksubstlist envlist []
    9.21 @@ -296,10 +296,6 @@
    9.22  
    9.23  fun second_pair (a,b,c) = (b,c);
    9.24  
    9.25 -fun one_of_three (a,b,c) = a;
    9.26 -fun two_of_three (a,b,c) = b;
    9.27 -fun three_of_three (a,b,c) = c;
    9.28 -
    9.29  (*************************)
    9.30  (* reconstruct res proof *)
    9.31  (*************************)
    10.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 08 10:50:02 2005 +0200
    10.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 08 18:43:39 2005 +0200
    10.3 @@ -2,6 +2,12 @@
    10.4  (* complete later *)
    10.5  (******************)
    10.6  
    10.7 +structure Recon_Transfer =
    10.8 +struct
    10.9 +
   10.10 +open Recon_Parse
   10.11 +infixr 8 ++; infixr 7 >>; infixr 6 ||;
   10.12 +
   10.13  fun not_newline ch = not (ch = "\n");
   10.14  
   10.15  
   10.16 @@ -19,7 +25,7 @@
   10.17  
   10.18  fun thm_of_string str = let val _ = set show_sorts
   10.19                                  val term = read str
   10.20 -                                val propterm = mk_Trueprop term
   10.21 +                                val propterm = HOLogic.mk_Trueprop term
   10.22                                  val cterm = cterm_of Mainsign propterm
   10.23                                  val _ = reset show_sorts
   10.24                              in
   10.25 @@ -113,7 +119,7 @@
   10.26  fun get_step_nums [] nums = nums
   10.27  |   get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num])
   10.28  
   10.29 -fun assoc_snd a [] = raise Noassoc
   10.30 +fun assoc_snd a [] = raise Recon_Base.Noassoc
   10.31    | assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t;
   10.32  
   10.33  (* change to be something using check_order  instead of a = y --> returns true if ASSERTION not raised in checkorder, false otherwise *)
   10.34 @@ -129,7 +135,7 @@
   10.35                                end
   10.36                                handle EXCEP => false
   10.37  
   10.38 -fun assoc_out_of_order a [] = raise Noassoc
   10.39 +fun assoc_out_of_order a [] = raise Recon_Base.Noassoc
   10.40  |   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
   10.41  
   10.42  fun get_assoc_snds [] xs assocs= assocs
   10.43 @@ -276,7 +282,7 @@
   10.44                                              val distfrees = distinct frees
   10.45  
   10.46                                              val metas = map make_meta_clause clauses
   10.47 -                                            val ax_strs = map (three_of_three ) axioms
   10.48 +                                            val ax_strs = map #3 axioms
   10.49  
   10.50                                              (* literals of -all- axioms, not just those used by spass *)
   10.51                                              val meta_strs = map get_meta_lits metas
   10.52 @@ -618,9 +624,6 @@
   10.53  (************************************************************)
   10.54  (* want to assume all axioms, then do haves for the other clauses*)
   10.55  (* then show for the last step *)
   10.56 -fun one_of_three (a,b,c) = a;
   10.57 -fun two_of_three (a,b,c) = b;
   10.58 -fun three_of_three (a,b,c) = c;
   10.59  
   10.60  (* replace ~ by not here *)
   10.61  fun change_nots [] = []
   10.62 @@ -809,3 +812,4 @@
   10.63                                 end 
   10.64  
   10.65  
   10.66 +end;
    11.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 08 10:50:02 2005 +0200
    11.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 08 18:43:39 2005 +0200
    11.3 @@ -25,7 +25,7 @@
    11.4                          else
    11.5                              add_in_order x (y::ys)
    11.6       
    11.7 -fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm));
    11.8 +fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
    11.9  
   11.10  Goal "False ==> False";
   11.11  by Auto_tac;
   11.12 @@ -81,7 +81,7 @@
   11.13  (****************************************)
   11.14  
   11.15   fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
   11.16 -                                     let val this_axiom =(assoc  clausenum clauses)
   11.17 +                                     let val this_axiom =(Recon_Base.assoc  clausenum clauses)
   11.18                                           val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
   11.19                                           val thmvars = thm_vars res
   11.20                                       in
   11.21 @@ -95,8 +95,8 @@
   11.22                   (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
   11.23  fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
   11.24          = let
   11.25 -              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
   11.26 -              val thm2 =  assoc  clause2 thml
   11.27 +              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
   11.28 +              val thm2 =  Recon_Base.assoc  clause2 thml
   11.29                val res =   thm1 RSN ((lit2 +1), thm2)
   11.30                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
   11.31                val thmvars = thm_vars res
   11.32 @@ -113,8 +113,8 @@
   11.33  
   11.34  fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
   11.35          = let
   11.36 -              val thm1 =  select_literal (lit1 + 1) (assoc  clause1 thml)
   11.37 -              val thm2 =  assoc  clause2 thml
   11.38 +              val thm1 =  select_literal (lit1 + 1) (Recon_Base.assoc  clause1 thml)
   11.39 +              val thm2 =  Recon_Base.assoc  clause2 thml
   11.40                val res =   thm1 RSN ((lit2 +1), thm2)
   11.41                val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
   11.42                val thmvars = thm_vars res
   11.43 @@ -156,13 +156,13 @@
   11.44  
   11.45  fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
   11.46                            let 
   11.47 -                            val th =  assoc clause thml
   11.48 +                            val th =  Recon_Base.assoc clause thml
   11.49                              val prems = prems_of th
   11.50                              val fac1 = get_nth (lit1+1) prems
   11.51                              val fac2 = get_nth (lit2+1) prems
   11.52 -                            val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)])
   11.53 +                            val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)])
   11.54                              val newenv = getnewenv unif_env
   11.55 -                            val envlist = alist_of newenv
   11.56 +                            val envlist = Envir.alist_of newenv
   11.57                              
   11.58                              val newsubsts = mksubstlist envlist []
   11.59                            in 
   11.60 @@ -201,32 +201,21 @@
   11.61  
   11.62  
   11.63  
   11.64 -fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm))
   11.65 -                             then 
   11.66 -                                  t
   11.67 -                             else 
   11.68 -                                 let val {Rand, Rator} = dest_comb t
   11.69 -                                 in
   11.70 -                                     get_unif_comb Rand eqterm
   11.71 -                                 end
   11.72 +fun get_unif_comb t eqterm =
   11.73 +    if ((type_of t) = (type_of eqterm))
   11.74 +    then t
   11.75 +    else
   11.76 +        let val _ $ rand = t
   11.77 +        in get_unif_comb rand eqterm end;
   11.78  
   11.79 -fun get_rhs_unif_lit t eqterm = if (can dest_eq t)
   11.80 -                            then 
   11.81 -                                let val {lhs, rhs} = dest_eq( t)
   11.82 -                                in
   11.83 -                                    rhs
   11.84 -                                end
   11.85 -                            else
   11.86 -                                get_unif_comb t eqterm
   11.87 -                         
   11.88 -fun get_lhs_unif_lit t eqterm = if (can dest_eq t)
   11.89 -                            then 
   11.90 -                                let val {lhs, rhs} = dest_eq( t)
   11.91 -                                in
   11.92 -                                    lhs
   11.93 -                                end
   11.94 -                            else
   11.95 -                                get_unif_comb t eqterm
   11.96 +fun get_unif_lit t eqterm =
   11.97 +    if (can HOLogic.dest_eq t)
   11.98 +    then
   11.99 +	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
  11.100 +	in lhs end
  11.101 +    else
  11.102 +	get_unif_comb t eqterm;
  11.103 +
  11.104  
  11.105  
  11.106  (*************************************)
  11.107 @@ -240,8 +229,8 @@
  11.108  (* have changed from negate_nead to negate_head.  God knows if this will actually work *)
  11.109  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
  11.110                            let 
  11.111 -                            val th1 =  assoc clause1 thml
  11.112 -                            val th2 =  assoc clause2 thml 
  11.113 +                            val th1 =  Recon_Base.assoc clause1 thml
  11.114 +                            val th2 =  Recon_Base.assoc clause2 thml 
  11.115                              val eq_lit_th = select_literal (lit1+1) th1
  11.116                              val mod_lit_th = select_literal (lit2+1) th2
  11.117                              val eqsubst = eq_lit_th RSN (2,rev_subst)
  11.118 @@ -263,8 +252,8 @@
  11.119  (*              
  11.120  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
  11.121                            let 
  11.122 -                            val th1 =  assoc clause1 thml
  11.123 -                            val th2 =  assoc clause2 thml 
  11.124 +                            val th1 =  Recon_Base.assoc clause1 thml
  11.125 +                            val th2 =  Recon_Base.assoc clause2 thml 
  11.126                              val eq_lit_th = select_literal (lit1+1) th1
  11.127                              val mod_lit_th = select_literal (lit2+1) th2
  11.128                              val eqsubst = eq_lit_th RSN (2,rev_subst)
  11.129 @@ -315,8 +304,8 @@
  11.130                      (* clause1, lit1 is thing to rewrite with *)
  11.131  fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
  11.132  
  11.133 -                          let val th1 =  assoc clause1 thml
  11.134 -                              val th2 = assoc clause2 thml
  11.135 +                          let val th1 =  Recon_Base.assoc clause1 thml
  11.136 +                              val th2 = Recon_Base.assoc clause2 thml
  11.137                                val eq_lit_th = select_literal (lit1+1) th1
  11.138                                val mod_lit_th = select_literal (lit2+1) th2
  11.139                                val eqsubst = eq_lit_th RSN (2,rev_subst)
  11.140 @@ -341,7 +330,7 @@
  11.141  
  11.142  
  11.143  fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
  11.144 -                           let val th1 =  assoc clause1 thml
  11.145 +                           let val th1 =  Recon_Base.assoc clause1 thml
  11.146                                 val prems1 = prems_of th1
  11.147                                 val newthm = refl RSN ((lit1+ 1), th1)
  11.148                                                 handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
  11.149 @@ -491,11 +480,6 @@
  11.150  
  11.151  fun second_pair (a,b,c) = (b,c);
  11.152  
  11.153 -fun one_of_three (a,b,c) = a;
  11.154 -fun two_of_three (a,b,c) = b;
  11.155 -fun three_of_three (a,b,c) = c;
  11.156 -
  11.157 -
  11.158  (* takes original axioms, proof_steps parsed from spass, variables *)
  11.159  
  11.160  fun translate_proof clauses proof allvars
    12.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Apr 08 10:50:02 2005 +0200
    12.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Apr 08 18:43:39 2005 +0200
    12.3 @@ -624,7 +624,7 @@
    12.4                                                           
    12.5                                                            in
    12.6                                                               Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    12.7 -                                                             apply_res_thm reconstr goalstring;
    12.8 +                                                             Recon_Transfer.apply_res_thm reconstr goalstring;
    12.9                                                               Pretty.writeln(Pretty.str  (oct_char "361"));
   12.10                                                               killWatcher childpid; () 
   12.11                                                            end
   12.12 @@ -651,7 +651,7 @@
   12.13  
   12.14                                                              (
   12.15                                                                   Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   12.16 -                                                                 apply_res_thm reconstr goalstring;
   12.17 +                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   12.18                                                                   Pretty.writeln(Pretty.str  (oct_char "361"));
   12.19                                                                   
   12.20                                                                   goals_being_watched := ((!goals_being_watched) - 1);
    13.1 --- a/src/HOL/Tools/reconstruction.ML	Fri Apr 08 10:50:02 2005 +0200
    13.2 +++ b/src/HOL/Tools/reconstruction.ML	Fri Apr 08 18:43:39 2005 +0200
    13.3 @@ -23,23 +23,6 @@
    13.4        in mksubstlist rest newlist end;
    13.5  
    13.6  
    13.7 -fun get_unif_comb t eqterm =
    13.8 -    if ((type_of t) = (type_of eqterm))
    13.9 -    then t
   13.10 -    else
   13.11 -        let val _ $ rand = t
   13.12 -        in get_unif_comb rand eqterm end;
   13.13 -
   13.14 -fun get_unif_lit t eqterm =
   13.15 -    if (can HOLogic.dest_eq t)
   13.16 -    then
   13.17 -	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
   13.18 -	in lhs end
   13.19 -    else
   13.20 -	get_unif_comb t eqterm;
   13.21 -
   13.22 -
   13.23 -
   13.24  (**** attributes ****)
   13.25  
   13.26  (** Binary resolution **)
    14.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Apr 08 10:50:02 2005 +0200
    14.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Apr 08 18:43:39 2005 +0200
    14.3 @@ -147,17 +147,48 @@
    14.4  by(Blast_tac 1);
    14.5  qed "Eq_TrueD1";
    14.6  
    14.7 +Goal "(True==P) ==> P";
    14.8 +by(Blast_tac 1);
    14.9 +qed "Eq_TrueD2";
   14.10 +
   14.11  Goal "(P=True) ==> P";
   14.12  by(Blast_tac 1);
   14.13 -qed "Eq_TrueD2";
   14.14 +qed "Eq_TrueD3";
   14.15  
   14.16  Goal "(P==False) ==> ~P";
   14.17  by(Blast_tac 1);
   14.18  qed "Eq_FalseD1";
   14.19  
   14.20 +Goal "(False==P) ==> ~P";
   14.21 +by(Blast_tac 1);
   14.22 +qed "Eq_FalseD2";
   14.23 +
   14.24  Goal "(P=False) ==> ~P";
   14.25  by(Blast_tac 1);
   14.26 -qed "Eq_FalseD2";
   14.27 +qed "Eq_FalseD3";
   14.28 +
   14.29 +
   14.30 +Goal "[|u == (if P then x else y); P|] ==> u==x";
   14.31 +by Auto_tac;
   14.32 +qed "eq_if_elim1";
   14.33 +
   14.34 +
   14.35 +Goal "[|u == (if P then x else y); ~P|] ==> u==y";
   14.36 +by Auto_tac;
   14.37 +qed"eq_if_elim2";
   14.38 +
   14.39 +
   14.40 +
   14.41 +fun resolve_or_id ths th =
   14.42 +     case [th] RL ths of
   14.43 +         []   => [th]
   14.44 +       | ths2 => ths2;
   14.45 +
   14.46 +
   14.47 +
   14.48 +val remove_bool_ths = [eq_if_elim1,eq_if_elim2,Eq_TrueD1,Eq_TrueD2,Eq_FalseD1,Eq_FalseD2];
   14.49 +
   14.50 +
   14.51  
   14.52  local 
   14.53  
   14.54 @@ -169,7 +200,10 @@
   14.55      "(P & True) == P", "(True & P) == P",
   14.56      "(False | P) == P", "(P | False) == P",
   14.57      "(False & P) == False", "(P & False) == False",
   14.58 -    "~True == False", "~False == True"];
   14.59 +    "~True == False", "~False == True"(*,
   14.60 +    "(False = P) == ~P", "(P = False) == ~P",
   14.61 +    "(True = P) == P",  "(P = True) == P"*)
   14.62 +    (*"(True ==> PROP P) == PROP P"*)];
   14.63  in
   14.64  
   14.65  val small_simpset = empty_ss addsimps small_simps
   14.66 @@ -194,6 +228,11 @@
   14.67  : Theory.theory -> ResClause.clause list list * Thm.thm list
   14.68  val rm_Eps 
   14.69  : (Term.term * Term.term) list -> Thm.thm list -> Term.term list
   14.70 +val claset_rules_of_thy : Theory.theory -> Thm.thm list
   14.71 +val simpset_rules_of_thy : Theory.theory -> Thm.thm list
   14.72 +val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
   14.73 +val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
   14.74 +
   14.75  end;
   14.76  
   14.77  structure ResAxioms : RES_AXIOMS =
   14.78 @@ -408,8 +447,9 @@
   14.79  fun cnf_simpset_rules [] err_list = ([],err_list)
   14.80    | cnf_simpset_rules (thm::thms) err_list =
   14.81      let val (ts,es) = cnf_simpset_rules thms err_list
   14.82 +	val thm' = resolve_or_id remove_bool_ths thm
   14.83      in
   14.84 -	((cnf_axiom thm)::ts,es) handle _ => (ts,(thm::es))
   14.85 +	((map cnf_axiom thm')@ts,es) handle _ => (ts,(thm::es))
   14.86      end;
   14.87  
   14.88  
   14.89 @@ -458,27 +498,7 @@
   14.90  	clausify_simpset_rules thms []
   14.91      end;
   14.92  
   14.93 -(* lcp-modified code *)
   14.94 -(*
   14.95 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
   14.96 -	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
   14.97 -
   14.98 -fun snds [] = []
   14.99 -   | snds ((x,y)::l) = y::(snds l);
  14.100 -
  14.101 -fun simpset_rules_of_thy thy =
  14.102 -     let val simpset = simpset_of thy
  14.103 -	val rules = #rules(fst (rep_ss simpset))
  14.104 -	val thms = retr_thms (snds(Net.dest rules))
  14.105 -     in	thms  end;
  14.106 -
  14.107 -print_depth 200;
  14.108 -simpset_rules_of_thy Main.thy;
  14.109  
  14.110  
  14.111  
  14.112 -
  14.113 -
  14.114 -*)
  14.115 -
  14.116  end;