diff options
author | Josh Chen | 2018-08-18 23:27:25 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-18 23:27:25 +0200 |
commit | 8833cdf99d3128466d85eb88aeb8e340e07e937c (patch) | |
tree | 87094caffe667540ac03cc05e9e1054c04a112d9 /Prod.thy | |
parent | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (diff) |
Reorganize methods
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -70,7 +70,7 @@ text "Rule attribute declarations---set up various methods to use the type rules lemmas Prod_comp [comp] = Prod_appl Prod_uniq lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 -lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim +lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \<open>Function composition\<close> @@ -97,7 +97,7 @@ and Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c" lemmas Unit_comp [comp] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim end |