equal
deleted
inserted
replaced
2 imports |
2 imports |
3 "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
3 "~~/src/HOL/Library/Predicate_Compile_Quickcheck" |
4 "~~/src/HOL/Library/Code_Prolog" |
4 "~~/src/HOL/Library/Code_Prolog" |
5 begin |
5 begin |
6 |
6 |
7 text \<open>An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"})\<close> |
7 text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close> |
8 text \<open>The example (original in Haskell) was imported with Haskabelle and |
8 text \<open>The example (original in Haskell) was imported with Haskabelle and |
9 manually slightly adapted. |
9 manually slightly adapted. |
10 \<close> |
10 \<close> |
11 |
11 |
12 datatype Nat = Zer |
12 datatype Nat = Zer |