equal
deleted
inserted
replaced
1 theory Simple_Inductive_Package |
1 theory Simple_Inductive_Package |
2 imports Main "../Base" |
2 imports Main "../Base" |
3 keywords "simple_inductive" :: thy_decl |
3 keywords "simple_inductive" :: thy_decl |
4 uses "simple_inductive_package.ML" |
|
5 begin |
4 begin |
|
5 |
|
6 ML_file "simple_inductive_package.ML" |
6 |
7 |
7 (* |
8 (* |
8 simple_inductive |
9 simple_inductive |
9 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
10 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
10 where |
11 where |