(* 
    ID:         $Id: BinGeneral.thy 2667 2006-09-26 07:15:00Z gklein $
    Author:     Jeremy Dawson, NICTA

*) 

theory bg imports Main 

begin

consts
  (* corresponding operations analysing bins *)
  bin_nth :: "int => nat => bool"

primrec
  Z : "bin_nth w 0 = True"
  Suc : "bin_nth w (Suc n) = False"

ML {*
use_legacy_bindings (the_context()) ;
*}

ML {*
val _ = ListPair.app bind_thm (["funpow_0", "funpow_Suc"], 
  thms "funpow.simps") ; 
*}

(* if this is deleted then bin_nth_0 below is recognised 
lemmas fs = funpow_Suc ;
*) 

ML {*
val _ = ListPair.app bind_thm (["bin_nth_0", "bin_nth_Suc"], bin_nth.simps) ;
  *}

lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;

end