equal
deleted
inserted
replaced
372 @{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad |
372 @{thm[mode=Rule] bs4[of "r\<^sub>1" "r\<^sub>2" _ "r\<^sub>3"]}\qquad |
373 @{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\ |
373 @{thm[mode=Rule] bs5[of "r\<^sub>3" "r\<^sub>4" _ "r\<^sub>1"]}\\ |
374 @{thm[mode=Axiom] bs6}\qquad |
374 @{thm[mode=Axiom] bs6}\qquad |
375 @{thm[mode=Axiom] bs7}\\ |
375 @{thm[mode=Axiom] bs7}\\ |
376 @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\ |
376 @{thm[mode=Rule] bs8[of "rs\<^sub>1" "rs\<^sub>2"]}\\ |
377 @{thm[mode=Axiom] ss1}\qquad |
377 %@ { t hm[mode=Axiom] ss1}\qquad |
378 @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad |
378 @{thm[mode=Rule] ss2[of "rs\<^sub>1" "rs\<^sub>2"]}\qquad |
379 @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\ |
379 @{thm[mode=Rule] ss3[of "r\<^sub>1" "r\<^sub>2"]}\\ |
380 @{thm[mode=Axiom] ss4}\qquad |
380 @{thm[mode=Axiom] ss4}\qquad |
381 @{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
381 @{thm[mode=Axiom] ss5[of "bs" "rs\<^sub>1" "rs\<^sub>2"]}\\ |
382 @{thm[mode=Rule] ss6[of "r\<^sub>1" "r\<^sub>2" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\ |
382 @{thm[mode=Rule] ss6[of "r\<^sub>1" "r\<^sub>2" "rs\<^sub>1" "rs\<^sub>2" "rs\<^sub>3"]}\\ |