diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Package/Simple_Inductive_Package.thy --- 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 \ 'a \ bool) \ 'a \ 'a \ bool" where @@ -16,6 +16,7 @@ thm trcl.induct thm trcl.intros +(* simple_inductive even and odd where