equal
deleted
inserted
replaced
177 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
177 @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"}, |
178 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
178 @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}] |
179 |
179 |
180 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
180 val eo_preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
181 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
181 val eo_prednames = [@{binding "even"}, @{binding "odd"}] |
182 val eo_syns = [NoSyn, NoSyn] |
182 val eo_mxs = [NoSyn, NoSyn] |
183 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
183 val eo_arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
184 val e_pred = @{term "even::nat\<Rightarrow>bool"} |
184 val e_pred = @{term "even::nat\<Rightarrow>bool"} |
185 val e_arg_tys = [@{typ "nat"}] |
185 val e_arg_tys = [@{typ "nat"}] |
186 |
186 |
187 |
187 |