ProgTutorial/Package/Simple_Inductive_Package.thy
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