# HG changeset patch
# User paulson
# Date 864306796 -7200
# Node ID 404fe31fd8d2c75e455f8cad4b74dd988b578946
# Parent  cdcc4d5602b671cae95b7d1577eac5dd5b7de8a8
New headers and other minor changes

diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/dcterm.sml
--- a/TFL/dcterm.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/dcterm.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/dcterm
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 (*---------------------------------------------------------------------------
  * Derived efficient cterm destructors.
  *---------------------------------------------------------------------------*)
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/mask.sig
--- a/TFL/mask.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/mask.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/mask
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 signature Mask_sig =
 sig
  datatype 'a binding = |-> of ('a * 'a)  (* infix 7 |->; *)
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/mask.sml
--- a/TFL/mask.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/mask.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/mask
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 (*---------------------------------------------------------------------------
  * This structure is intended to shield TFL from any constructors already 
  * declared in the environment. In the Isabelle port, for example, there
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/post.sml
--- a/TFL/post.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/post.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,6 +1,13 @@
+(*  Title:      TFL/post
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Postprocessing of TFL definitions
+*)
+
 (*-------------------------------------------------------------------------
-there are 3 postprocessors that get applied to the definition:
-
+Three postprocessors are applied to the definition:
     - a wellfoundedness prover (WF_TAC)
     - a simplifier (tries to eliminate the language of termination expressions)
     - a termination prover
@@ -75,7 +82,7 @@
                                     addss (!simpset)) 1);
 
  val simpls = [less_eq RS eq_reflection,
-               lex_prod_def, rprod_def, measure_def, inv_image_def];
+               lex_prod_def, measure_def, inv_image_def];
 
  (*---------------------------------------------------------------------------
   * Does some standard things with the termination conditions of a definition:
@@ -191,14 +198,14 @@
           |   e                 => print_exn e;
 
 
-(*lcp: uncurry the predicate of the induction rule*)
-fun uncurry_rule rl = Prod_Syntax.split_rule_var
+(*lcp: curry the predicate of the induction rule*)
+fun curry_rule rl = Prod_Syntax.split_rule_var
                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
 			 rl);
 
 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
 val meta_outer = 
-    uncurry_rule o standard o 
+    curry_rule o standard o 
     rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
 				  ORELSE' etac conjE));
 
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/rules.new.sml
--- a/TFL/rules.new.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/rules.new.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/rules
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Emulation of HOL inference rules for TFL
+*)
+
 structure FastRules : Rules_sig = 
 struct
 
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/rules.sig
--- a/TFL/rules.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/rules.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/rules
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Emulation of HOL inference rules for TFL
+*)
+
 signature Rules_sig =
 sig
 (*  structure USyntax : USyntax_sig *)
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/sys.sml
--- a/TFL/sys.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/sys.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,4 +1,10 @@
-(* Compile the TFL system *)
+(*  Title:      TFL/mask
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Compile the TFL system
+*)
 
 (* Portability stuff *)
 nonfix prefix;
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/tfl.sig
--- a/TFL/tfl.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/tfl.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/tfl
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Main TFL functor
+*)
+
 signature TFL_sig =
 sig
    structure Rules: Rules_sig
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/thms.sig
--- a/TFL/thms.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/thms.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/thms
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 signature Thms_sig =
 sig
    val WF_INDUCTION_THM:thm
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/thms.sml
--- a/TFL/thms.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/thms.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/thms
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 structure Thms : Thms_sig =
 struct
    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/thry.sig
--- a/TFL/thry.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/thry.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/thry
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 signature Thry_sig =
 sig
   type 'a binding
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/thry.sml
--- a/TFL/thry.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/thry.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,9 @@
+(*  Title:      TFL/thry
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+*)
+
 structure Thry : Thry_sig (* LThry_sig *) = 
 struct
 
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/usyntax.sig
--- a/TFL/usyntax.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/usyntax.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/usyntax
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Emulation of HOL's abstract syntax functions
+*)
+
 signature USyntax_sig =
 sig
   structure Utils : Utils_sig
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/usyntax.sml
--- a/TFL/usyntax.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/usyntax.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/usyntax
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Emulation of HOL's abstract syntax functions
+*)
+
 structure USyntax : USyntax_sig =
 struct
 
@@ -104,7 +112,6 @@
 
 
 (* Construction routines *)
-(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)
 fun mk_var{Name,Ty} = Free(Name,Ty);
 val mk_prim_var = Var;
 
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/utils.sig
--- a/TFL/utils.sig	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/utils.sig	Thu May 22 15:13:16 1997 +0200
@@ -1,3 +1,11 @@
+(*  Title:      TFL/utils
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Basic utilities
+*)
+
 signature Utils_sig =
 sig
   (* General error format and reporting mechanism *)
diff -r cdcc4d5602b6 -r 404fe31fd8d2 TFL/utils.sml
--- a/TFL/utils.sml	Thu May 22 15:11:56 1997 +0200
+++ b/TFL/utils.sml	Thu May 22 15:13:16 1997 +0200
@@ -1,7 +1,10 @@
-(*---------------------------------------------------------------------------
- * Some common utilities.
- *---------------------------------------------------------------------------*)
+(*  Title:      TFL/utils
+    ID:         $Id$
+    Author:     Konrad Slind, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
 
+Basic utilities
+*)
 
 structure Utils = 
 struct