TFL/post.sml
changeset 3302 404fe31fd8d2
parent 3271 b873969b05d3
child 3331 c81c7f8ad333
--- 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));