equal
deleted
inserted
replaced

1 

2 (* Author: Florian Haftmann, TU Muenchen *) 

3 

4 header {* A huge collection of equations to generate code from *} 

5 

6 theory Candidates 

7 imports 

8 Complex_Main 

9 Library 

10 List_Prefix 

11 "~~/src/HOL/Number_Theory/Primes" 

12 "~~/src/HOL/ex/Records" 

13 begin 

14 

15 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where 

16 empty: "sublist [] xs" 

17  drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" 

18  take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)" 

19 

20 code_pred sublist . 

21 

22 (*avoid popular infix*) 

23 code_reserved SML upto 

24 

25 end 