Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 459 020e27417b59
parent 458 44a70e69ef92
child 461 40c9fb60de3c
child 462 0911d3aabf47
equal deleted inserted replaced
458:44a70e69ef92 459:020e27417b59 
   945     (* reflexivity of operators arising from Cong_tac *)
 
   945     (* reflexivity of operators arising from Cong_tac *)
 
   946     NDT ctxt "8" (rtac @{thm refl}),
 
   946     NDT ctxt "8" (rtac @{thm refl}),
 
   947 
   947 
   948     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
 
   948     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
 
   949     (* observe ---> *) 
   949     (* observe ---> *) 
   950     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
   950     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
   951                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
   951                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
   952 
   952 
   953     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
 
   953     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
 
   954     NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
   954     NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
   955                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
   955                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
nominal2