equal
deleted
inserted
replaced
111 |
111 |
112 fun HTT_coinduct3_tac ctxt s i = |
112 fun HTT_coinduct3_tac ctxt s i = |
113 res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i |
113 res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i |
114 |
114 |
115 val HTTgenIs = |
115 val HTTgenIs = |
116 map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono}) |
116 map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono}) |
117 ["true : HTTgen(R)", |
117 ["true : HTTgen(R)", |
118 "false : HTTgen(R)", |
118 "false : HTTgen(R)", |
119 "[| a : R; b : R |] ==> <a,b> : HTTgen(R)", |
119 "[| a : R; b : R |] ==> <a,b> : HTTgen(R)", |
120 "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", |
120 "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)", |
121 "one : HTTgen(R)", |
121 "one : HTTgen(R)", |