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.
Quot/quotient_tacs.ML
changeset 761 e2ac18492c68
parent 758 3104d62e7a16
child 762 baac4639ecef
equal deleted inserted replaced
760:c1989de100b4 761:e2ac18492c68 
   562              "", "does not match with original theorem", rtrm_str]
 
   562              "", "does not match with original theorem", rtrm_str]
 
   563 in
 
   563 in
 
   564   error msg
 
   564   error msg
 
   565 end
 
   565 end
 
   566 
   566 
       
   567 open Quotient_Term;
 
   567  
   568  
   568 fun procedure_inst ctxt rtrm qtrm =
 
   569 fun procedure_inst ctxt rtrm qtrm =
 
   569 let
 
   570 let
 
   570   val thy = ProofContext.theory_of ctxt
 
   571   val thy = ProofContext.theory_of ctxt
 
   571   val rtrm' = HOLogic.dest_Trueprop rtrm
 
   572   val rtrm' = HOLogic.dest_Trueprop rtrm
nominal2