equal
deleted
inserted
replaced
6 theory Codegenerator_Candidates |
6 theory Codegenerator_Candidates |
7 imports |
7 imports |
8 Complex_Main |
8 Complex_Main |
9 AssocList |
9 AssocList |
10 Binomial |
10 Binomial |
|
11 "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" |
|
12 Dlist |
11 Fset |
13 Fset |
12 Enum |
14 Enum |
13 List_Prefix |
15 List_Prefix |
14 Nat_Infinity |
16 Nat_Infinity |
15 Nested_Environment |
17 Nested_Environment |
16 Option_ord |
18 Option_ord |
17 Permutation |
19 Permutation |
18 "~~/src/HOL/Number_Theory/Primes" |
20 "~~/src/HOL/Number_Theory/Primes" |
19 Product_ord |
21 Product_ord |
|
22 "~~/src/HOL/ex/Records" |
20 SetsAndFunctions |
23 SetsAndFunctions |
21 Tree |
24 Tree |
22 While_Combinator |
25 While_Combinator |
23 Word |
26 Word |
24 "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" |
|
25 "~~/src/HOL/ex/Records" |
|
26 begin |
27 begin |
27 |
28 |
28 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
29 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where |
29 empty: "sublist [] xs" |
30 empty: "sublist [] xs" |
30 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |
31 | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)" |