--- 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.
*---------------------------------------------------------------------------*)
--- 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 |->; *)
--- 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
--- 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));
--- 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
--- 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 *)
--- 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;
--- 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
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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;
--- 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 *)
--- 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