src/CCL/Hered.thy
changeset 32010 cb1a1c94b4cd
parent 28262 aa7ca36d67fd
child 32153 a0e57fb1b930
equal deleted inserted replaced
32009:fd3c60ad9155 32010:cb1a1c94b4cd
     1 (*  Title:      CCL/Hered.thy
     1 (*  Title:      CCL/Hered.thy
     2     ID:         $Id$
       
     3     Author:     Martin Coen
     2     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     3     Copyright   1993  University of Cambridge
     5 *)
     4 *)
     6 
     5 
     7 header {* Hereditary Termination -- cf. Martin Lo\"f *}
     6 header {* Hereditary Termination -- cf. Martin Lo\"f *}
   111 
   110 
   112 fun HTT_coinduct3_tac ctxt s i =
   111 fun HTT_coinduct3_tac ctxt s i =
   113   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
   112   res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i
   114 
   113 
   115 val HTTgenIs =
   114 val HTTgenIs =
   116   map (mk_genIs (the_context ()) @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   115   map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono})
   117   ["true : HTTgen(R)",
   116   ["true : HTTgen(R)",
   118    "false : HTTgen(R)",
   117    "false : HTTgen(R)",
   119    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
   118    "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
   120    "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
   119    "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
   121    "one : HTTgen(R)",
   120    "one : HTTgen(R)",