equal
deleted
inserted
replaced
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 |