src/HOL/ex/Fib.ML
changeset 5537 c2bd39a2c0ee
parent 5143 b94cd208f073
child 6916 4957978b6f9e
equal deleted inserted replaced
5536:130f3d891fb2 5537:c2bd39a2c0ee
    63 by (ALLGOALS  (*using [fib_Suc_Suc] here results in a longer proof!*)
    63 by (ALLGOALS  (*using [fib_Suc_Suc] here results in a longer proof!*)
    64     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
    64     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
    65 				       mod_less, mod_Suc])));
    65 				       mod_less, mod_Suc])));
    66 by (ALLGOALS
    66 by (ALLGOALS
    67     (asm_full_simp_tac
    67     (asm_full_simp_tac
    68      (simpset() addsimps ([] @ add_ac @ mult_ac @
    68      (simpset() addsimps add_ac @ mult_ac @
    69 			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    69 			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    70 			  mod_less, mod_Suc]))));
    70 			  mod_less, mod_Suc])));
    71 qed "fib_Cassini";
    71 qed "fib_Cassini";
    72 
    72 
    73 
    73 
    74 (** Towards Law 6.111 of Concrete Mathematics **)
    74 (** Towards Law 6.111 of Concrete Mathematics **)
    75 
    75