equal
deleted
inserted
replaced
1 (* Title: HOL/Decision_Procs/Cooper.thy |
1 (* Title: HOL/Decision_Procs/Cooper.thy |
2 Author: Amine Chaieb |
2 Author: Amine Chaieb |
3 *) |
3 *) |
4 |
4 |
5 theory Cooper |
5 theory Cooper |
6 imports Complex_Main Efficient_Nat |
6 imports Complex_Main "~~/src/HOL/Library/Efficient_Nat" |
7 uses ("cooper_tac.ML") |
7 uses ("cooper_tac.ML") |
8 begin |
8 begin |
9 |
9 |
10 function iupt :: "int \<Rightarrow> int \<Rightarrow> int list" where |
10 function iupt :: "int \<Rightarrow> int \<Rightarrow> int list" where |
11 "iupt i j = (if j < i then [] else i # iupt (i+1) j)" |
11 "iupt i j = (if j < i then [] else i # iupt (i+1) j)" |