| changeset 66810 | cc2b490f9dc4 |
| parent 66386 | 962c12353c67 |
| child 66816 | 212a3334e7da |
| 66809:f6a30d48aab0 | 66810:cc2b490f9dc4 |
|---|---|
7 section \<open>Natural numbers\<close> |
7 section \<open>Natural numbers\<close> |
8 |
8 |
9 theory Nat |
9 theory Nat |
10 imports Inductive Typedef Fun Rings |
10 imports Inductive Typedef Fun Rings |
11 begin |
11 begin |
12 |
|
13 named_theorems arith "arith facts -- only ground formulas" |
|
14 ML_file "Tools/arith_data.ML" |
|
15 |
|
16 |
12 |
17 subsection \<open>Type \<open>ind\<close>\<close> |
13 subsection \<open>Type \<open>ind\<close>\<close> |
18 |
14 |
19 typedecl ind |
15 typedecl ind |
20 |
16 |