equal
deleted
inserted
replaced
130 @{thm[display]"nat_less_induct"[no_vars]} |
130 @{thm[display]"nat_less_induct"[no_vars]} |
131 As an application, we prove a property of the following |
131 As an application, we prove a property of the following |
132 function: |
132 function: |
133 *}; |
133 *}; |
134 |
134 |
135 consts f :: "nat \<Rightarrow> nat"; |
135 axiomatization f :: "nat \<Rightarrow> nat" |
136 axioms f_ax: "f(f(n)) < f(Suc(n))"; |
136 where f_ax: "f(f(n)) < f(Suc(n))" |
137 |
137 |
138 text{* |
138 text{* |
139 \begin{warn} |
139 \begin{warn} |
140 We discourage the use of axioms because of the danger of |
140 We discourage the use of axioms because of the danger of |
141 inconsistencies. Axiom @{text f_ax} does |
141 inconsistencies. Axiom @{text f_ax} does |