equal
deleted
inserted
replaced
4 section \<open>A huge collection of equations to generate code from\<close> |
4 section \<open>A huge collection of equations to generate code from\<close> |
5 |
5 |
6 theory Candidates |
6 theory Candidates |
7 imports |
7 imports |
8 Complex_Main |
8 Complex_Main |
9 "~~/src/HOL/Library/Library" |
9 "HOL-Library.Library" |
10 "~~/src/HOL/Library/Subseq_Order" |
10 "HOL-Library.Subseq_Order" |
11 "~~/src/HOL/Library/RBT" |
11 "HOL-Library.RBT" |
12 "~~/src/HOL/Data_Structures/Tree_Map" |
12 "HOL-Data_Structures.Tree_Map" |
13 "~~/src/HOL/Data_Structures/Tree_Set" |
13 "HOL-Data_Structures.Tree_Set" |
14 "~~/src/HOL/Computational_Algebra/Computational_Algebra" |
14 "HOL-Computational_Algebra.Computational_Algebra" |
15 "~~/src/HOL/Computational_Algebra/Polynomial_Factorial" |
15 "HOL-Computational_Algebra.Polynomial_Factorial" |
16 "~~/src/HOL/Number_Theory/Eratosthenes" |
16 "HOL-Number_Theory.Eratosthenes" |
17 "~~/src/HOL/ex/Records" |
17 "HOL-ex.Records" |
18 begin |
18 begin |
19 |
19 |
20 text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
20 text \<open>Drop technical stuff from @{theory Quickcheck_Narrowing} which is tailored towards Haskell\<close> |
21 |
21 |
22 setup \<open> |
22 setup \<open> |