src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17315 5bf0e0aacc24
parent 17312 159783c74f75
child 17317 3f12de2e2e6e
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 16:09:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 17:35:02 2005 +0200
     1.3 @@ -137,13 +137,7 @@
     1.4  fun thmstrings [] str = str
     1.5  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
     1.6  
     1.7 -fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
     1.8 -
     1.9 -
    1.10 -
    1.11 -fun retrieve_axioms clause_arr  [] = []
    1.12 -|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
    1.13 - 						     (retrieve_axioms clause_arr  xs)
    1.14 +fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
    1.15  
    1.16  fun subone x = x - 1
    1.17  
    1.18 @@ -160,7 +154,7 @@
    1.19  	val _ = TextIO.output(axnums,(numstr clasimp_nums))
    1.20  	val _ = TextIO.closeOut(axnums)*)
    1.21      in
    1.22 -	retrieve_axioms clause_arr clasimp_nums
    1.23 +	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
    1.24      end
    1.25  
    1.26  
    1.27 @@ -187,9 +181,18 @@
    1.28        clasimp_names
    1.29     end
    1.30     
    1.31 - fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
    1.32 -   get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    1.33 -                       thms clause_arr num_of_clauses;
    1.34 +
    1.35 +fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
    1.36 +  let (* parse spass proof into datatype *)
    1.37 +      val tokens = #1(lex proofstr)
    1.38 +      val proof_steps = parse tokens
    1.39 +      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
    1.40 +                         ("Did parsing on "^proofstr)
    1.41 +      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    1.42 +  in
    1.43 +    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    1.44 +                    thms clause_arr num_of_clauses
    1.45 +  end;
    1.46      
    1.47   fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    1.48     get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
    1.49 @@ -207,49 +210,49 @@
    1.50  
    1.51  fun addvars c (a,b)  = (a,b,c)
    1.52  
    1.53 - fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.54 -     let 
    1.55 -	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.56 -	val axioms = (List.filter is_axiom) proof_steps
    1.57 -	val step_nums = get_step_nums axioms []
    1.58 +fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    1.59 +  let 
    1.60 +     val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.61 +     val axioms = (List.filter is_axiom) proof_steps
    1.62 +     val step_nums = get_step_nums axioms []
    1.63  
    1.64 -	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    1.65 -	
    1.66 -	val vars = map thm_vars clauses
    1.67 -       
    1.68 -	val distvars = distinct (fold append vars [])
    1.69 -	val clause_terms = map prop_of clauses  
    1.70 -	val clause_frees = List.concat (map term_frees clause_terms)
    1.71 +     val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    1.72 +     
    1.73 +     val vars = map thm_vars clauses
    1.74 +    
    1.75 +     val distvars = distinct (fold append vars [])
    1.76 +     val clause_terms = map prop_of clauses  
    1.77 +     val clause_frees = List.concat (map term_frees clause_terms)
    1.78  
    1.79 -	val frees = map lit_string_with_nums clause_frees;
    1.80 +     val frees = map lit_string_with_nums clause_frees;
    1.81  
    1.82 -	val distfrees = distinct frees
    1.83 +     val distfrees = distinct frees
    1.84  
    1.85 -	val metas = map Meson.make_meta_clause clauses
    1.86 -	val ax_strs = map #3 axioms
    1.87 +     val metas = map Meson.make_meta_clause clauses
    1.88 +     val ax_strs = map #3 axioms
    1.89  
    1.90 -	(* literals of -all- axioms, not just those used by spass *)
    1.91 -	val meta_strs = map ReconOrderClauses.get_meta_lits metas
    1.92 -       
    1.93 -	val metas_and_strs = ListPair.zip (metas,meta_strs)
    1.94 -	val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
    1.95 -	val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
    1.96 +     (* literals of -all- axioms, not just those used by spass *)
    1.97 +     val meta_strs = map ReconOrderClauses.get_meta_lits metas
    1.98 +    
    1.99 +     val metas_and_strs = ListPair.zip (metas,meta_strs)
   1.100 +     val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
   1.101 +     val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
   1.102  
   1.103 -	(* get list of axioms as thms with their variables *)
   1.104 +     (* get list of axioms as thms with their variables *)
   1.105  
   1.106 -	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   1.107 -	val ax_vars = map thm_vars ax_metas
   1.108 -	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   1.109 +     val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   1.110 +     val ax_vars = map thm_vars ax_metas
   1.111 +     val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   1.112  
   1.113 -	(* get list of extra axioms as thms with their variables *)
   1.114 -	val extra_metas = add_if_not_inlist metas ax_metas []
   1.115 -	val extra_vars = map thm_vars extra_metas
   1.116 -	val extra_with_vars = if (not (extra_metas = []) ) 
   1.117 -			      then ListPair.zip (extra_metas,extra_vars)
   1.118 -			      else []
   1.119 -     in
   1.120 -	(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   1.121 -     end;
   1.122 +     (* get list of extra axioms as thms with their variables *)
   1.123 +     val extra_metas = add_if_not_inlist metas ax_metas []
   1.124 +     val extra_vars = map thm_vars extra_metas
   1.125 +     val extra_with_vars = if (not (extra_metas = []) ) 
   1.126 +			   then ListPair.zip (extra_metas,extra_vars)
   1.127 +			   else []
   1.128 +  in
   1.129 +     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
   1.130 +  end;
   1.131                                              
   1.132  
   1.133  (*********************************************************************)
   1.134 @@ -257,122 +260,24 @@
   1.135  (* Get out reconstruction steps as a string to be sent to Isabelle   *)
   1.136  (*********************************************************************)
   1.137  
   1.138 -
   1.139  fun rules_to_string [] = "NONE"
   1.140    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
   1.141 -                                  
   1.142 -
   1.143 -(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
   1.144 -\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
   1.145 -\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
   1.146 -\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
   1.147 -\1454[0:Obv:1453.0] ||  -> .";*)
   1.148  
   1.149  fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
   1.150  
   1.151  val remove_linebreaks = subst_for #"\n" #"\t";
   1.152  val restore_linebreaks = subst_for #"\t" #"\n";
   1.153  
   1.154 -fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.155 -  let val _ = File.append(File.tmp_path (Path.basic"thmstringfile"))
   1.156 -                  ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses))
   1.157 -
   1.158 -     (***********************************)
   1.159 -     (* parse spass proof into datatype *)
   1.160 -     (***********************************)
   1.161 -      val tokens = #1(lex proofstr)
   1.162 -      val proof_steps = parse tokens
   1.163 -      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
   1.164 -                         ("Did parsing on "^proofstr)
   1.165 -      val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring"))
   1.166 -                        ("Parsing for thmstring: "^thmstring)
   1.167 -      (************************************)
   1.168 -      (* recreate original subgoal as thm *)
   1.169 -      (************************************)
   1.170 -    
   1.171 -      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   1.172 -      (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   1.173 -      (* subgoal this is, and turn it into meta_clauses *)
   1.174 -      (* should prob add array and table here, so that we can get axioms*)
   1.175 -      (* produced from the clasimpset rather than the problem *)
   1.176 -
   1.177 -      val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses
   1.178 -      val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
   1.179 -                   rules_to_string axiom_names 
   1.180 -      val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
   1.181 -                         ("reconstring is: "^ax_str^"  "^goalstring)       
   1.182 -  in 
   1.183 -       TextIO.output (toParent, ax_str^"\n");
   1.184 -       TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.185 -       TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.186 -       TextIO.flushOut toParent;
   1.187 -
   1.188 -       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.189 -      (* Attempt to prevent several signals from turning up simultaneously *)
   1.190 -       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.191 -  end
   1.192 -  handle _ => 
   1.193 -  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.194 -  in 
   1.195 -     TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
   1.196 -       TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
   1.197 -       TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
   1.198 -       TextIO.flushOut toParent;
   1.199 -      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.200 -      (* Attempt to prevent several signals from turning up simultaneously *)
   1.201 -      Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.202 -  end
   1.203  
   1.204 -
   1.205 -fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.206 +fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax = 
   1.207   let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
   1.208 -               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
   1.209 -                "goalstr is: "^goalstring^" num of clauses is: "^
   1.210 -                (string_of_int num_of_clauses))
   1.211 -
   1.212 -    (***********************************)
   1.213 -    (* get vampire axiom names         *)
   1.214 -    (***********************************)
   1.215 -
   1.216 -     val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses
   1.217 -     val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
   1.218 -                  rules_to_string axiom_names
   1.219 -    in 
   1.220 -	 File.append(File.tmp_path (Path.basic "reconstrfile")) 
   1.221 -	            ("reconstring is: "^ax_str^"  "^goalstring);
   1.222 -         TextIO.output (toParent, ax_str^"\n");
   1.223 -	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   1.224 -	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   1.225 -	 TextIO.flushOut toParent;
   1.226 +               ("thmstring is " ^ thmstring ^ 
   1.227 +                "\nproofstr is " ^ proofstr ^
   1.228 +                "\ngoalstr is " ^ goalstring ^
   1.229 +                "\nnum of clauses is " ^ string_of_int num_of_clauses)
   1.230  
   1.231 -	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.232 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.233 -	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.234 -    end
   1.235 -    handle _ => 
   1.236 -    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.237 -    in 
   1.238 -	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.239 -	 TextIO.output (toParent, thmstring^"\n");
   1.240 -	 TextIO.output (toParent, goalstring^"\n");
   1.241 -	 TextIO.flushOut toParent;
   1.242 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.243 -	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.244 -    end;
   1.245 -
   1.246 -
   1.247 -fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.248 - let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
   1.249 -               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
   1.250 -                "goalstr is: "^goalstring^" num of clauses is: "^
   1.251 -                (string_of_int num_of_clauses))
   1.252 -
   1.253 -    (***********************************)
   1.254 -    (* get E axiom names         *)
   1.255 -    (***********************************)
   1.256 -
   1.257 -     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
   1.258 -     val ax_str = "Rules from clasimpset used in proof found by E: " ^
   1.259 +     val axiom_names = getax proofstr thms clause_arr num_of_clauses
   1.260 +     val ax_str = "Rules from clasimpset used in automatic proof: " ^
   1.261                    rules_to_string axiom_names
   1.262      in 
   1.263  	 File.append(File.tmp_path (Path.basic "reconstrfile"))
   1.264 @@ -386,18 +291,29 @@
   1.265  	(* Attempt to prevent several signals from turning up simultaneously *)
   1.266  	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
   1.267      end
   1.268 -    handle _ => 
   1.269 -    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
   1.270 -    in 
   1.271 -	TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
   1.272 -	 TextIO.output (toParent, thmstring^"\n");
   1.273 -	 TextIO.output (toParent, goalstring^"\n");
   1.274 -	 TextIO.flushOut toParent;
   1.275 -	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.276 -	(* Attempt to prevent several signals from turning up simultaneously *)
   1.277 -	Posix.Process.sleep(Time.fromSeconds 1); all_tac
   1.278 -    end;
   1.279 +    handle _ => (*FIXME: exn handler is too general!*)
   1.280 +     (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
   1.281 +      TextIO.output (toParent, "Proof found but translation failed : " ^ 
   1.282 +                     remove_linebreaks proofstr ^ "\n");
   1.283 +      TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
   1.284 +      TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
   1.285 +      TextIO.flushOut toParent;
   1.286 +      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   1.287 +      (* Attempt to prevent several signals from turning up simultaneously *)
   1.288 +      Posix.Process.sleep(Time.fromSeconds 1); all_tac);
   1.289  
   1.290 +fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
   1.291 +      clause_arr num_of_clauses  = 
   1.292 +  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
   1.293 +       clause_arr num_of_clauses get_axiom_names_vamp_E;
   1.294 +
   1.295 +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
   1.296 +      clause_arr  num_of_clauses  = 
   1.297 +  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
   1.298 +       clause_arr num_of_clauses get_axiom_names_spass;
   1.299 +
   1.300 +
   1.301 +(**** Full proof reconstruction for SPASS (not really working) ****)
   1.302  
   1.303  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   1.304    let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
   1.305 @@ -792,29 +708,15 @@
   1.306  (* be passed over to the watcher, e.g.  numcls25       *)
   1.307  (*******************************************************)
   1.308  
   1.309 -(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
   1.310 -
   1.311 -val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   1.312 -
   1.313 -val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)";
   1.314 -
   1.315 -
   1.316 -val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
   1.317 -
   1.318 -val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
   1.319 -*)
   1.320 +fun apply_res_thm str goalstring  = 
   1.321 +  let val tokens = #1 (lex str);
   1.322 +      val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
   1.323 +	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   1.324 +      val (frees,recon_steps) = parse_step tokens 
   1.325 +      val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   1.326 +      val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str
   1.327 +  in 
   1.328 +     Pretty.writeln(Pretty.str isar_str)
   1.329 +  end 
   1.330  
   1.331 -fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
   1.332 -				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
   1.333 -			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
   1.334 -                                   val (frees,recon_steps) = parse_step tokens 
   1.335 -                                   val isar_str = to_isar_proof (frees, recon_steps, goalstring)
   1.336 -                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
   1.337 -                               in 
   1.338 -                                  TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
   1.339 -                               end 
   1.340 -
   1.341 -
   1.342 -(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
   1.343 -*)
   1.344  end;