changeset 562 | daf404920ab9 |
parent 538 | e9fd5eff62c1 |
--- a/ProgTutorial/Package/Simple_Inductive_Package.thy Fri Jun 03 15:15:17 2016 +0100 +++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Tue May 14 11:10:53 2019 +0200 @@ -5,7 +5,7 @@ ML_file "simple_inductive_package.ML" -(* + simple_inductive trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" where @@ -16,6 +16,7 @@ thm trcl.induct thm trcl.intros +(* simple_inductive even and odd where