equal
deleted
inserted
replaced
1 (* ID: $Id$ *) |
|
2 (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*) |
1 (*<*)theory Advanced imports Even uses "../../antiquote_setup.ML" begin(*>*) |
3 |
2 |
4 text {* |
3 text {* |
5 The premises of introduction rules may contain universal quantifiers and |
4 The premises of introduction rules may contain universal quantifiers and |
6 monotone functions. A universal quantifier lets the rule |
5 monotone functions. A universal quantifier lets the rule |
358 *} |
357 *} |
359 |
358 |
360 (*<*) |
359 (*<*) |
361 |
360 |
362 text{*the following declaration isn't actually used*} |
361 text{*the following declaration isn't actually used*} |
363 consts integer_arity :: "integer_op \<Rightarrow> nat" |
|
364 primrec |
362 primrec |
365 "integer_arity (Number n) = 0" |
363 integer_arity :: "integer_op \<Rightarrow> nat" |
366 "integer_arity UnaryMinus = 1" |
364 where |
367 "integer_arity Plus = 2" |
365 "integer_arity (Number n) = 0" |
|
366 | "integer_arity UnaryMinus = 1" |
|
367 | "integer_arity Plus = 2" |
368 |
368 |
369 text{* the rest isn't used: too complicated. OK for an exercise though.*} |
369 text{* the rest isn't used: too complicated. OK for an exercise though.*} |
370 |
370 |
371 inductive_set |
371 inductive_set |
372 integer_signature :: "(integer_op * (unit list * unit)) set" |
372 integer_signature :: "(integer_op * (unit list * unit)) set" |