tunings of some comments (nothing serious)
authorurbanc
Tue Nov 01 23:54:29 2005 +0100 (2005-11-01)
changeset 18052004515accc10
parent 18051 dba086ed50cb
child 18053 2719a6b7d95e
tunings of some comments (nothing serious)
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_permeq.ML
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Oct 31 16:35:15 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Nov 01 23:54:29 2005 +0100
     1.3 @@ -9,21 +9,24 @@
     1.4  (*      tuple_lambda [a] t       produces %a . t                              *) 
     1.5  (*      tuple_lambda [a,b,c] t   produces %(a,b,c). t                         *)
     1.6  
     1.7 -  fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
     1.8 -    | tuple_lambda [x] t = lambda x t
     1.9 -    | tuple_lambda (x::xs) t =
    1.10 -       let
    1.11 -         val t' = tuple_lambda xs t;
    1.12 -         val Type ("fun", [T,U]) = fastype_of t';
    1.13 -       in
    1.14 -         HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
    1.15 -       end; 
    1.16 +fun tuple_lambda [] t  = Abs ("x", HOLogic.unitT, t)
    1.17 +  | tuple_lambda [x] t = lambda x t
    1.18 +  | tuple_lambda (x::xs) t =
    1.19 +    let
    1.20 +        val t' = tuple_lambda xs t;
    1.21 +        val Type ("fun", [T,U]) = fastype_of t';
    1.22 +    in
    1.23 +        HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
    1.24 +    end; 
    1.25  
    1.26  fun find_var frees name =
    1.27    (case Library.find_first (equal name o fst o dest_Free) frees of
    1.28      NONE => error ("No such Variable in term: " ^ quote name)
    1.29    | SOME v => v);
    1.30  
    1.31 +(* - names specifies the variables that are involved in the *)
    1.32 +(*   induction                                              *)
    1.33 +(* - rule is the induction rule to be applied               *)              
    1.34  fun nominal_induct_tac (names, rule) facts state =
    1.35    let
    1.36      val sg     = Thm.sign_of_thm state;
    1.37 @@ -38,7 +41,7 @@
    1.38          val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
    1.39          val (P :: ts, x) = split_last concl_vars
    1.40            handle Empty => error "Malformed conclusion of induction rule"
    1.41 -            | Bind => error "Malformed conclusion of induction rule";
    1.42 +               | Bind  => error "Malformed conclusion of induction rule";
    1.43        in
    1.44          cterm_instantiate
    1.45            ((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Oct 31 16:35:15 2005 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Nov 01 23:54:29 2005 +0100
     2.3 @@ -103,11 +103,6 @@
     2.4  
     2.5  in             
     2.6  
     2.7 -(* FIXME simp_modifiers' 
     2.8 -
     2.9 -(Markus needs to commit this)
    2.10 -*)
    2.11 -
    2.12  
    2.13  fun simp_meth_setup tac =
    2.14    Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)