changeset 51674 | 2b1498a2ce85 |
parent 51673 | 4dfa00e264d8 |
child 51678 | 1e33b81c328a |
--- a/src/HOL/Inductive.thy Tue Jan 22 14:33:45 2013 +0100 +++ b/src/HOL/Inductive.thy Fri Apr 05 22:08:42 2013 +0200 @@ -275,6 +275,7 @@ ML_file "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup consts + case_guard :: "'a \<Rightarrow> 'a" case_nil :: "'a \<Rightarrow> 'b" case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"