src/HOL/NatDef.ML
changeset 2680 20fa49e610ca
parent 2608 450c9b682a92
child 2718 460fd0f8d478
equal deleted inserted replaced
2679:3eac428cdd1b 2680:20fa49e610ca
   680 (*** eliminates ~= in premises, which trans_tac cannot deal with ***)
   680 (*** eliminates ~= in premises, which trans_tac cannot deal with ***)
   681 qed_goal "nat_neqE" thy
   681 qed_goal "nat_neqE" thy
   682   "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
   682   "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P"
   683   (fn major::prems => [cut_facts_tac [less_linear] 1,
   683   (fn major::prems => [cut_facts_tac [less_linear] 1,
   684                        REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
   684                        REPEAT(eresolve_tac ([disjE,major RS notE]@prems) 1)]);
       
   685 
       
   686 
       
   687 
       
   688 (* add function nat_add_primrec *) 
       
   689 val (_, nat_add_primrec) = Datatype.add_datatype
       
   690 ([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([], "nat")], NoSyn)]) HOL.thy;
       
   691