# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272180396 -7200
# Node ID 5abac261b5ce11f891380e86e3eb41af3a719dff
# Parent  51f411b1197d8532ba23ab2000d1eb0b3d065a7d
tuned

diff -r 51f411b1197d -r 5abac261b5ce Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Sun Apr 25 09:13:16 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Sun Apr 25 09:26:36 2010 +0200
@@ -9,7 +9,7 @@
 sig
   val equivariance: string -> Proof.context -> local_theory
   val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
-  val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
+  val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
 end
 
 structure Nominal_Eqvt : NOMINAL_EQVT =
@@ -27,9 +27,10 @@
 
 
 (** 
- proves F[f t] from F[t] which is the given theorem  
+ given the theorem F[t]; proves the theorem F[f t] 
+
   - F needs to be monotone
-  - f returns either SOME for a term it fires 
+  - f returns either SOME for a term it fires on 
     and NONE elsewhere 
 **)
 fun map_term f t = 
@@ -90,7 +91,7 @@
 val perm_cancel = @{thms permute_minus_cancel(2)}
 val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
 
-fun eqvt_rel_case_tac ctxt pred_names pi intro  = 
+fun eqvt_rel_single_case_tac ctxt pred_names pi intro  = 
 let
   val thy = ProofContext.theory_of ctxt
   val cpi = Thm.cterm_of thy (mk_minus pi)
@@ -113,7 +114,7 @@
 
 fun eqvt_rel_tac ctxt pred_names pi induct intros =
 let
-  val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros
+  val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
 in
   EVERY' (rtac induct :: cases)
 end
@@ -150,9 +151,10 @@
   val raw_induct = atomize_induct ctxt raw_induct
   val intros = map atomize_intr intrs
   val params_no = length (Inductive.params_of raw_induct)
-  val (([raw_concl], [raw_pi]), ctxt') = ctxt 
-         |> Variable.import_terms false [concl_of raw_induct] 
-         ||>> Variable.variant_fixes ["p"]
+  val (([raw_concl], [raw_pi]), ctxt') = 
+    ctxt 
+    |> Variable.import_terms false [concl_of raw_induct] 
+    ||>> Variable.variant_fixes ["p"]
   val pi = Free (raw_pi, @{typ perm})
   val preds = map (fst o HOLogic.dest_imp)
     (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
@@ -171,7 +173,7 @@
 
 val _ =
   OuterSyntax.local_theory "equivariance"
-    "prove equivariance for inductive predicate involving nominal datatypes" 
+    "Proves equivariance for inductive predicate involving nominal datatypes." 
       K.thy_decl (P.xname >> equivariance);
 end;