" ^ title ^ " of " ^ tname ^ "

# HG changeset patch # User paulson # Date 849088456 -3600 # Node ID dacee519738a44b7dbd76a6e0977f4c8766d526f # Parent 3ebeaaacfbd1a51d670ef266281136036e763b46 Converted I/O operatios for Basis Library compatibility diff -r 3ebeaaacfbd1 -r dacee519738a src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Wed Nov 27 10:52:31 1996 +0100 +++ b/src/Pure/Thy/thy_read.ML Wed Nov 27 10:54:16 1996 +0100 @@ -160,12 +160,13 @@ structures inherit this value.) *) val gif_path = ref (tack_on ("/" ^ - space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))) + space_implode "/" (rev (tl (tl (rev (space_explode "/" + (OS.FileSys.getDir ()))))))) "Tools"); (*Path of Isabelle's main directory*) val base_path = ref ( - "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (pwd ()))))))); + "/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ()))))))); (** HTML variables **) @@ -181,7 +182,7 @@ (*HTML file of theory currently being read (Initialized by thyfile2html; used by use_thy and store_thm)*) -val cur_htmlfile = ref None : outstream option ref; +val cur_htmlfile = ref None : TextIO.outstream option ref; (*Boolean variable which indicates if the title "Theorems proved in foo.ML" has already been inserted into the current HTML file*) @@ -192,18 +193,18 @@ -(*Make name of the output ML file for a theory *) +(*Make name of the TextIO.output ML file for a theory *) fun out_name tname = "." ^ tname ^ ".thy.ML"; (*Read a file specified by thy_file containing theory thy *) fun read_thy tname thy_file = let - val instream = open_in thy_file; - val outstream = open_out (out_name tname); + val instream = TextIO.openIn thy_file; + val outstream = TextIO.openOut (out_name tname); in - output (outstream, ThySyn.parse tname (input (instream, 999999))); - close_out outstream; - close_in instream + TextIO.output (outstream, ThySyn.parse tname (TextIO.inputAll instream)); + TextIO.closeOut outstream; + TextIO.closeIn instream end; fun file_exists file = (file_info file <> ""); @@ -286,7 +287,7 @@ fun get_filenames path name = let fun new_filename () = let val found = find_file path (name ^ ".thy"); - val absolute_path = absolute_path (pwd ()); + val absolute_path = absolute_path (OS.FileSys.getDir ()); val thy_file = absolute_path found; val (thy_path, _) = split_filename thy_file; val found = find_file path (name ^ ".ML"); @@ -389,7 +390,7 @@ index_path: relative path to directory containing main theory chart *) fun mk_charthead file tname title repeats gif_path index_path package = - output (file, + TextIO.output (file, "" ^ title ^ " of " ^ tname ^ "\n

" ^ title ^ " of theory " ^ tname ^ "

\nThe name of every theory is linked to its theory file
\n" ^ @@ -499,8 +500,8 @@ (** Make chart of super-theories **) - val sup_out = open_out (tack_on tpath ("." ^ tname ^ "_sup.html")); - val sub_out = open_out (tack_on tpath ("." ^ tname ^ "_sub.html")); + val sup_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sup.html")); + val sub_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sub.html")); (*Theories that already have been listed in this chart*) val listed = ref []; @@ -528,7 +529,7 @@ | mk_offset (l::ls) cur = implode (replicate (l - cur) " ") ^ "| " ^ mk_offset ls (l+1); - in output (sup_out, + in TextIO.output (sup_out, " " ^ mk_offset continued 0 ^ "\\__" ^ (if is_pure then t else " s mem wanted_theories) (parents_of_name tname); in mk_entry relatives end; in if is_some (!cur_htmlfile) then - (close_out (the (!cur_htmlfile)); + (TextIO.closeOut (the (!cur_htmlfile)); warning "Last theory's HTML file has not been closed.") else (); - cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html"))); + cur_htmlfile := Some (TextIO.openOut (tack_on tpath ("." ^ tname ^ ".html"))); cur_has_title := false; - output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); + TextIO.output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path package; - output(sup_out, + TextIO.output(sup_out, "" ^ tname ^ " \ \ $\\/$ \n"); list_ancestors tname 0 []; - output (sup_out, "

"); - close_out sup_out; + TextIO.output (sup_out, "

"); + TextIO.closeOut sup_out; mk_charthead sub_out tname "Children" false gif_path rel_index_path package; - output(sub_out, + TextIO.output(sub_out, "" ^ tname ^ " \ \ $\\/$ \n"); - close_out sub_out + TextIO.closeOut sub_out end; (*Invoke every put method stored in a theory's methods table to initialize @@ -694,11 +695,11 @@ val fname = tack_on path ("." ^ t ^ "_sub.html"); val out = if file_exists fname then - open_append fname handle e => + TextIO.openAppend fname handle e => (warning ("Unable to write to file " ^ fname); raise e) else raise MK_HTML; - in output (out, + in TextIO.output (out, " |\n \\__" ^ tname ^ " \ @@ -707,11 +708,11 @@ \\ \ $/\\$ \n"); - close_out out + TextIO.closeOut out end; val theory_list = - open_append (tack_on (!index_path) ".theory_list.txt") + TextIO.openAppend (tack_on (!index_path) ".theory_list.txt") handle _ => (make_html := false; writeln ("Warning: Cannot write to " ^ (!index_path) ^ " while making HTML files.\n\ @@ -719,8 +720,8 @@ \Call init_html() from within a \ \writeable directory to reactivate it."); raise MK_HTML) - in output (theory_list, tname ^ " " ^ abs_path ^ "\n"); - close_out theory_list; + in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n"); + TextIO.closeOut theory_list; robust_seq add_to_parents new_parents end @@ -761,7 +762,7 @@ in map store_thm_db axioms end; if not (!delete_tmpfiles) then () - else delete_file (out_name tname); + else OS.FileSys.remove (out_name tname); if not (!make_html) then () else thyfile2html abs_path tname @@ -798,8 +799,8 @@ (*Close HTML file*) case !cur_htmlfile of - Some out => (output (out, "

\n"); - close_out out; + Some out => (TextIO.output (out, "

\n"); + TextIO.closeOut out; cur_htmlfile := None) | None => () ) @@ -1064,7 +1065,7 @@ fun mk_theorems_title out = if not (!cur_has_title) then (cur_has_title := true; - output (out, "

Theorems proved in

Theorems proved in " ^ (!cur_thyname) ^ ".ML:

\n")) else (); @@ -1095,10 +1096,10 @@ in case !cur_htmlfile of Some out => (mk_theorems_title out; - output (out, "

" ^ name ^ "\n

" ^
+                TextIO.output (out, "" ^ name ^ "\n" ^
                              escape 
-			      (explode 
-			       (string_of_thm (#1 (freeze_thaw thm)))) ^
+                              (explode 
+                               (string_of_thm (#1 (freeze_thaw thm)))) ^
                              "
\n")
                )
            | None => ()
@@ -1173,16 +1174,16 @@
 
 (*Init HTML generator by setting paths and creating new files*)
 fun init_html () =
-  let val cwd = pwd();
+  let val cwd = OS.FileSys.getDir();
 
-      val theory_list = close_out (open_out ".theory_list.txt");
+      val theory_list = TextIO.closeOut (TextIO.openOut ".theory_list.txt");
 
       val rel_gif_path = relative_path cwd (!gif_path);
 
       (*Make new HTML files for Pure and CPure*)
       fun init_pure_html () =
-        let val pure_out = open_out ".Pure_sub.html";
-            val cpure_out = open_out ".CPure_sub.html";
+        let val pure_out = TextIO.openOut ".Pure_sub.html";
+            val cpure_out = TextIO.openOut ".CPure_sub.html";
             val package =
               if cwd subdir_of (!base_path) then
                 relative_path (!base_path) cwd
@@ -1191,10 +1192,10 @@
                         package;
            mk_charthead cpure_out "CPure" "Children" false rel_gif_path ""
                         package;
-           output (pure_out, "Pure\n");
-           output (cpure_out, "CPure\n");
-           close_out pure_out;
-           close_out cpure_out;
+           TextIO.output (pure_out, "Pure\n");
+           TextIO.output (cpure_out, "CPure\n");
+           TextIO.closeOut pure_out;
+           TextIO.closeOut cpure_out;
            pure_subchart := Some cwd
         end;
   in make_html := true;
@@ -1202,9 +1203,9 @@
 
      (*Make sure that base_path contains the physical path and no
        symbolic links*)
-     cd (!base_path);
-     base_path := pwd();
-     cd cwd;
+     OS.FileSys.chDir (!base_path);
+     base_path := OS.FileSys.getDir();
+     OS.FileSys.chDir cwd;
 
      if cwd subdir_of (!base_path) then ()
      else warning "The current working directory seems to be no \
@@ -1221,9 +1222,9 @@
 (*Generate index.html*)
 fun finish_html () = if not (!make_html) then () else
   let val tlist_path = tack_on (!index_path) ".theory_list.txt";
-      val theory_list = open_in tlist_path;
-      val theories = space_explode "\n" (input (theory_list, 999999));
-      val dummy = (close_in theory_list; delete_file tlist_path);
+      val theory_list = TextIO.openIn tlist_path;
+      val theories = space_explode "\n" (TextIO.inputAll theory_list);
+      val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path);
 
       val gif_path = relative_path (!index_path) (!gif_path);
 
@@ -1243,7 +1244,7 @@
            ".html\">" ^ tname ^ "
\n"
         end;
 
-      val out = open_out (tack_on (!index_path) "index.html");
+      val out = TextIO.openOut (tack_on (!index_path) "index.html");
 
       (*Find out in which subdirectory of Isabelle's main directory the
         index.html is placed; if index_path is no subdirectory of base_path
@@ -1269,25 +1270,25 @@
 
       (*Add link to current directory to 'super' index.html*)
       fun link_directory () =
-        let val old_index = open_in (super_index ^ "/index.html");
-            val content = rev (explode (input (old_index, 999999)));
-            val dummy = close_in old_index;
+        let val old_index = TextIO.openIn (super_index ^ "/index.html");
+            val content = rev (explode (TextIO.inputAll old_index));
+            val dummy = TextIO.closeIn old_index;
 
-            val out = open_append (super_index ^ "/index.html");
+            val out = TextIO.openAppend (super_index ^ "/index.html");
             val rel_path = space_implode "/" (drop (level, subdirs));
         in 
-           output (out,
+           TextIO.output (out,
              (if nth_elem (3, content) <> "!" then ""
               else "\n
Subdirectories:\n") ^
              "" ^ rel_path ^
              "\n");
-           close_out out
+           TextIO.closeOut out
         end;
 
      (*If index_path is no subdirectory of base_path then the title should
        not contain the string "Isabelle/"*)
      val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir;
-  in output (out,
+  in TextIO.output (out,
        "" ^ title ^ "\n\
        \" ^ title ^ "\n\
        \The name of every theory is linked to its theory file
\n\
@@ -1309,7 +1310,7 @@
           "
View the ReadMe file.\n"
         else "") ^
        "
" ^ implode (map main_entry theories) ^ "");
-     close_out out;
+     TextIO.closeOut out;
      if super_index = "" orelse (inside_isabelle andalso level = 0) then ()
         else link_directory ()
   end;
@@ -1318,7 +1319,7 @@
 fun section s =
   case !cur_htmlfile of
       Some out => (mk_theorems_title out;
-                   output (out, "" ^ s ^ "\n"))
+                   TextIO.output (out, "" ^ s ^ "\n"))
     | None => ();
 
 
@@ -1354,7 +1355,7 @@
 
 (*Add file to thy_reader_files list*)
 fun set_thy_reader_file file =
-  let val file' = absolute_path (pwd ()) file;
+  let val file' = absolute_path (OS.FileSys.getDir ()) file;
   in thy_reader_files := file' :: (!thy_reader_files) end;
 
 (*Add file and also 'use' it*)
@@ -1377,12 +1378,12 @@
 local
 
   fun gen_use_dir use_cmd dirname =
-    let val old_dir = pwd ();
-    in cd dirname;
+    let val old_dir = OS.FileSys.getDir ();
+    in OS.FileSys.chDir dirname;
        if !make_html then init_html() else ();
        use_cmd "ROOT.ML";
        finish_html();
-       cd old_dir
+       OS.FileSys.chDir old_dir
     end;
 
 in
diff -r 3ebeaaacfbd1 -r dacee519738a src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Wed Nov 27 10:52:31 1996 +0100
+++ b/src/Pure/tctical.ML	Wed Nov 27 10:54:16 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	tctical
+(*  Title:      tctical
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Tacticals
@@ -15,53 +15,53 @@
 signature TACTICAL =
   sig
   type tactic  (* = thm -> thm Sequence.seq*)
-  val all_tac		: tactic
-  val ALLGOALS		: (int -> tactic) -> tactic   
-  val APPEND		: tactic * tactic -> tactic
-  val APPEND'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val CHANGED		: tactic -> tactic
-  val COND		: (thm -> bool) -> tactic -> tactic -> tactic   
-  val DETERM		: tactic -> tactic
-  val EVERY		: tactic list -> tactic   
-  val EVERY'		: ('a -> tactic) list -> 'a -> tactic
-  val EVERY1		: (int -> tactic) list -> tactic
-  val FILTER		: (thm -> bool) -> tactic -> tactic
-  val FIRST		: tactic list -> tactic   
-  val FIRST'		: ('a -> tactic) list -> 'a -> tactic
-  val FIRST1		: (int -> tactic) list -> tactic
-  val FIRSTGOAL		: (int -> tactic) -> tactic
-  val goals_limit	: int ref
-  val INTLEAVE		: tactic * tactic -> tactic
-  val INTLEAVE'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val METAHYPS		: (thm list -> tactic) -> int -> tactic
-  val no_tac		: tactic
-  val ORELSE		: tactic * tactic -> tactic
-  val ORELSE'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val pause_tac		: tactic
-  val print_tac		: tactic
-  val REPEAT		: tactic -> tactic
-  val REPEAT1		: tactic -> tactic
-  val REPEAT_DETERM_N	: int -> tactic -> tactic
-  val REPEAT_DETERM	: tactic -> tactic
-  val REPEAT_DETERM1	: tactic -> tactic
+  val all_tac           : tactic
+  val ALLGOALS          : (int -> tactic) -> tactic   
+  val APPEND            : tactic * tactic -> tactic
+  val APPEND'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val CHANGED           : tactic -> tactic
+  val COND              : (thm -> bool) -> tactic -> tactic -> tactic   
+  val DETERM            : tactic -> tactic
+  val EVERY             : tactic list -> tactic   
+  val EVERY'            : ('a -> tactic) list -> 'a -> tactic
+  val EVERY1            : (int -> tactic) list -> tactic
+  val FILTER            : (thm -> bool) -> tactic -> tactic
+  val FIRST             : tactic list -> tactic   
+  val FIRST'            : ('a -> tactic) list -> 'a -> tactic
+  val FIRST1            : (int -> tactic) list -> tactic
+  val FIRSTGOAL         : (int -> tactic) -> tactic
+  val goals_limit       : int ref
+  val INTLEAVE          : tactic * tactic -> tactic
+  val INTLEAVE'         : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val METAHYPS          : (thm list -> tactic) -> int -> tactic
+  val no_tac            : tactic
+  val ORELSE            : tactic * tactic -> tactic
+  val ORELSE'           : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val pause_tac         : tactic
+  val print_tac         : tactic
+  val REPEAT            : tactic -> tactic
+  val REPEAT1           : tactic -> tactic
+  val REPEAT_DETERM_N   : int -> tactic -> tactic
+  val REPEAT_DETERM     : tactic -> tactic
+  val REPEAT_DETERM1    : tactic -> tactic
   val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic
   val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
-  val REPEAT_FIRST	: (int -> tactic) -> tactic
-  val REPEAT_SOME	: (int -> tactic) -> tactic
-  val SELECT_GOAL	: tactic -> int -> tactic
-  val SOMEGOAL		: (int -> tactic) -> tactic   
-  val STATE		: (thm -> tactic) -> tactic
-  val strip_context	: term -> (string * typ) list * term list * term
-  val SUBGOAL		: ((term*int) -> tactic) -> int -> tactic
-  val suppress_tracing	: bool ref
-  val THEN		: tactic * tactic -> tactic
-  val THEN'		: ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
-  val THEN_ELSE		: tactic * (tactic*tactic) -> tactic
-  val traced_tac	: (thm -> (thm * thm Sequence.seq) option) -> tactic
-  val tracify		: bool ref -> tactic -> thm -> thm Sequence.seq
-  val trace_REPEAT	: bool ref
-  val TRY		: tactic -> tactic
-  val TRYALL		: (int -> tactic) -> tactic   
+  val REPEAT_FIRST      : (int -> tactic) -> tactic
+  val REPEAT_SOME       : (int -> tactic) -> tactic
+  val SELECT_GOAL       : tactic -> int -> tactic
+  val SOMEGOAL          : (int -> tactic) -> tactic   
+  val STATE             : (thm -> tactic) -> tactic
+  val strip_context     : term -> (string * typ) list * term list * term
+  val SUBGOAL           : ((term*int) -> tactic) -> int -> tactic
+  val suppress_tracing  : bool ref
+  val THEN              : tactic * tactic -> tactic
+  val THEN'             : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
+  val THEN_ELSE         : tactic * (tactic*tactic) -> tactic
+  val traced_tac        : (thm -> (thm * thm Sequence.seq) option) -> tactic
+  val tracify           : bool ref -> tactic -> thm -> thm Sequence.seq
+  val trace_REPEAT      : bool ref
+  val TRY               : tactic -> tactic
+  val TRYALL            : (int -> tactic) -> tactic   
   end;
 
 
@@ -91,7 +91,7 @@
   Does not backtrack to tac2 if tac1 was initially chosen. *)
 fun (tac1 ORELSE tac2) st =
     case Sequence.pull(tac1 st) of
-	None       => tac2 st
+        None       => tac2 st
       | sequencecell => Sequence.seqof(fn()=> sequencecell);
 
 
@@ -100,22 +100,22 @@
   The tactic tac2 is not applied until needed.*)
 fun (tac1 APPEND tac2) st = 
   Sequence.append(tac1 st,
-		  Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+                  Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
 
 (*Like APPEND, but interleaves results of tac1 and tac2.*)
 fun (tac1 INTLEAVE tac2) st = 
     Sequence.interleave(tac1 st,
-			Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
+                        Sequence.seqof(fn()=> Sequence.pull (tac2 st)));
 
 (*Conditional tactic.
-	tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
-	tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
+        tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)
+        tac1 THEN tac2   = tac1 THEN_ELSE (tac2, no_tac)
 *)
 fun (tac THEN_ELSE (tac1, tac2)) st = 
     case Sequence.pull(tac st) of
-	None    => tac2 st		(*failed; try tactic 2*)
-      | seqcell => Sequence.flats 	(*succeeded; use tactic 1*)
-	            (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
+        None    => tac2 st              (*failed; try tactic 2*)
+      | seqcell => Sequence.flats       (*succeeded; use tactic 1*)
+                    (Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell)));
 
 
 (*Versions for combining tactic-valued functions, as in
@@ -135,7 +135,7 @@
 (*Make a tactic deterministic by chopping the tail of the proof sequence*)
 fun DETERM tac st =  
       case Sequence.pull (tac st) of
-	      None => Sequence.null
+              None => Sequence.null
             | Some(x,_) => Sequence.cons(x, Sequence.null);
 
 
@@ -182,7 +182,7 @@
 (*Pause until a line is typed -- if non-empty then fail. *)
 fun pause_tac st =  
   (prs"** Press RETURN to continue: ";
-   if input(std_in,1) = "\n" then Sequence.single st
+   if TextIO.inputLine TextIO.stdIn = "\n" then Sequence.single st
    else (prs"Goodbye\n";  Sequence.null));
 
 exception TRACE_EXIT of thm
@@ -194,7 +194,7 @@
 
 (*Handle all tracing commands for current state and tactic *)
 fun exec_trace_command flag (tac, st) = 
-   case input_line(std_in) of
+   case TextIO.inputLine(TextIO.stdIn) of
        "\n" => tac st
      | "f\n" => Sequence.null
      | "o\n" => (flag:=false;  tac st)
@@ -215,15 +215,15 @@
 fun tracify flag tac st =
   if !flag andalso not (!suppress_tracing)
            then (!print_goals_ref (!goals_limit) st;  
-		 prs"** Press RETURN to continue: ";
-		 exec_trace_command flag (tac,st))
+                 prs"** Press RETURN to continue: ";
+                 exec_trace_command flag (tac,st))
   else tac st;
 
 (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
 fun traced_tac seqf st = 
     (suppress_tracing := false;
      Sequence.seqof (fn()=> seqf st
-		         handle TRACE_EXIT st' => Some(st', Sequence.null)));
+                         handle TRACE_EXIT st' => Some(st', Sequence.null)));
 
 
 (*Deterministic REPEAT: only retains the first outcome; 
@@ -232,10 +232,10 @@
 fun REPEAT_DETERM_N n tac = 
   let val tac = tracify trace_REPEAT tac
       fun drep 0 st = Some(st, Sequence.null)
-	| drep n st =
-	   (case Sequence.pull(tac st) of
-		None       => Some(st, Sequence.null)
-	      | Some(st',_) => drep (n-1) st')
+        | drep n st =
+           (case Sequence.pull(tac st) of
+                None       => Some(st, Sequence.null)
+              | Some(st',_) => drep (n-1) st')
   in  traced_tac (drep n)  end;
 
 (*Allows any number of repetitions*)
@@ -245,12 +245,12 @@
 fun REPEAT tac = 
   let val tac = tracify trace_REPEAT tac
       fun rep qs st = 
-	case Sequence.pull(tac st) of
-  	    None       => Some(st, Sequence.seqof(fn()=> repq qs))
+        case Sequence.pull(tac st) of
+            None       => Some(st, Sequence.seqof(fn()=> repq qs))
           | Some(st',q) => rep (q::qs) st'
       and repq [] = None
         | repq(q::qs) = case Sequence.pull q of
-  	    None       => repq qs
+            None       => repq qs
           | Some(st,q) => rep (q::qs) st
   in  traced_tac (rep [])  end;
 
@@ -276,13 +276,13 @@
   Essential to work backwards since tac(i) may add/delete subgoals at i. *)
 fun ALLGOALS tac st = 
   let fun doall 0 = all_tac
-	| doall n = tac(n) THEN doall(n-1)
+        | doall n = tac(n) THEN doall(n-1)
   in  doall(nprems_of st)st  end;
 
 (*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1)  *)
 fun SOMEGOAL tac st = 
   let fun find 0 = no_tac
-	| find n = tac(n) ORELSE find(n-1)
+        | find n = tac(n) ORELSE find(n-1)
   in  find(nprems_of st)st  end;
 
 (*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).
@@ -334,9 +334,9 @@
       val ct_eq_x = mk_prop_equals (ct, xfree)
       and refl_ct = reflexive ct
       fun restore th = 
-	  implies_elim 
-	    (forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th)))
-	    refl_ct
+          implies_elim 
+            (forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th)))
+            refl_ct
   in  (equal_elim
          (combination (combination refl_implies refl_ct) (assume ct_eq_x))
          (trivial ct),
@@ -348,7 +348,7 @@
 fun select tac st0 i =
   let val cprem::_ = drop(i-1, cprems_of st0)
       val (eq_cprem, restore) = (*we hope maxidx goes to ~1*)
-	                        eq_trivial (adjust_maxidx cprem)
+                                eq_trivial (adjust_maxidx cprem)
       fun next st = bicompose false (false, restore st, nprems_of st) i st0
   in  Sequence.flats (Sequence.maps next (tac eq_cprem))
   end;
@@ -361,13 +361,13 @@
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    new proof state by enclosing them by a universal quantification *)
 fun protect_subgoal st i =
-	Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
-	handle _ => error"SELECT_GOAL -- impossible error???";
+        Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st)
+        handle _ => error"SELECT_GOAL -- impossible error???";
 
 fun SELECT_GOAL tac i st = 
   case (i, drop(i-1, prems_of st)) of
       (_,[]) => Sequence.null
-    | (1,[_]) => tac st		(*If i=1 and only one subgoal do nothing!*)
+    | (1,[_]) => tac st         (*If i=1 and only one subgoal do nothing!*)
     | (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i
     | (_, _::_) => select tac st i;
 
@@ -377,10 +377,10 @@
   Main difference from strip_assums concerns parameters: 
     it replaces the bound variables by free variables.  *)
 fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 
-	strip_context_aux (params, H::Hs, B)
+        strip_context_aux (params, H::Hs, B)
   | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
         let val (b,u) = variant_abs(a,T,t)
-	in  strip_context_aux ((b,T)::params, Hs, u)  end
+        in  strip_context_aux ((b,T)::params, Hs, u)  end
   | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
 
 fun strip_context A = strip_context_aux ([],[],A);
@@ -409,7 +409,7 @@
 
   fun free_of s ((a,i), T) =
         Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i),
-	     T)
+             T)
 
   fun mk_inst (var as Var(v,T))  = (var,  free_of "METAHYP1_" (v,T))
 in
@@ -431,17 +431,17 @@
       (*Subgoal variables: make Free; lift type over params*)
       fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
           if var mem concl_vars 
-	  then (var, true, free_of "METAHYP2_" (v,T))
-	  else (var, false,
-		free_of "METAHYP2_" (v, map #2 params --->T))
+          then (var, true, free_of "METAHYP2_" (v,T))
+          else (var, false,
+                free_of "METAHYP2_" (v, map #2 params --->T))
       (*Instantiate subgoal vars by Free applied to params*)
       fun mk_ctpair (t,in_concl,u) = 
-	  if in_concl then (cterm t,  cterm u)
+          if in_concl then (cterm t,  cterm u)
           else (cterm t,  cterm (list_comb (u,fparams)))
       (*Restore Vars with higher type and index*)
       fun mk_subgoal_swap_ctpair 
-		(t as Var((a,i),_), in_concl, u as Free(_,U)) = 
-	  if in_concl then (cterm u, cterm t)
+                (t as Var((a,i),_), in_concl, u as Free(_,U)) = 
+          if in_concl then (cterm u, cterm t)
           else (cterm u, cterm(Var((a, i+maxidx), U)))
       (*Embed B in the original context of params and hyps*)
       fun embed B = list_all_free (params, Logic.list_implies (hyps, B))
@@ -449,34 +449,34 @@
       fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
       (*Embed an ff pair in the original params*)
       fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), 
-					     list_abs_free (params, u))
+                                             list_abs_free (params, u))
       (*Remove parameter abstractions from the ff pairs*)
       fun elim_ff ff = flexpair_abs_elim_list cparams ff
       (*A form of lifting that discharges assumptions.*)
       fun relift st = 
-	let val prop = #prop(rep_thm st)
-	    val subgoal_vars = (*Vars introduced in the subgoals*)
-		  foldr add_term_vars (Logic.strip_imp_prems prop, [])
-	    and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
-	    val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
-	    val st' = instantiate ([], map mk_ctpair subgoal_insts) st
-	    val emBs = map (cterm o embed) (prems_of st')
+        let val prop = #prop(rep_thm st)
+            val subgoal_vars = (*Vars introduced in the subgoals*)
+                  foldr add_term_vars (Logic.strip_imp_prems prop, [])
+            and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
+            val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
+            val st' = instantiate ([], map mk_ctpair subgoal_insts) st
+            val emBs = map (cterm o embed) (prems_of st')
             and ffs = map (cterm o embed_ff) (tpairs_of st')
-	    val Cth  = implies_elim_list st' 
-			    (map (elim_ff o assume) ffs @
-			     map (elim o assume) emBs)
-	in  (*restore the unknowns to the hypotheses*)
-	    free_instantiate (map swap_ctpair insts @
-			      map mk_subgoal_swap_ctpair subgoal_insts)
-		(*discharge assumptions from state in same order*)
-		(implies_intr_list (ffs@emBs)
-		  (forall_intr_list cparams (implies_intr_list chyps Cth)))
-	end
+            val Cth  = implies_elim_list st' 
+                            (map (elim_ff o assume) ffs @
+                             map (elim o assume) emBs)
+        in  (*restore the unknowns to the hypotheses*)
+            free_instantiate (map swap_ctpair insts @
+                              map mk_subgoal_swap_ctpair subgoal_insts)
+                (*discharge assumptions from state in same order*)
+                (implies_intr_list (ffs@emBs)
+                  (forall_intr_list cparams (implies_intr_list chyps Cth)))
+        end
       val subprems = map (forall_elim_vars 0) hypths
       and st0 = trivial (cterm concl)
       (*function to replace the current subgoal*)
       fun next st = bicompose false (false, relift st, nprems_of st)
-	            i state
+                    i state
   in  Sequence.flats (Sequence.maps next (tacf subprems st0))
   end;
 end;

" ^ title ^ " of theory " ^ tname ^ "

Theorems proved in " ^ (!cur_thyname) ^ ".ML:

Subdirectories:

" ^ rel_path ^ "

" ^ title ^ "

" ^ s ^ "

" ^ s ^ "