Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/BaseDefinitions/termC.sml
changeset 60320 02102eaa2021
parent 60317 638d02a9a96a
child 60322 2220bafba61f
equal deleted inserted replaced
60319:2edbed71fde6 60320:02102eaa2021 
     4 *)
 
     4 *)
 
     5 
     5 
     6 "-----------------------------------------------------------------------------------------------";
 
     6 "-----------------------------------------------------------------------------------------------";
 
     7 "table of contents -----------------------------------------------------------------------------";
 
     7 "table of contents -----------------------------------------------------------------------------";
 
     8 "-----------------------------------------------------------------------------------------------";
 
     8 "-----------------------------------------------------------------------------------------------";
 
       
     9 "----------- fun is_atom -----------------------------------------------------------------------";
 
     9 "----------- numerals in Isabelle2011/12/13 -------------";
 
    10 "----------- numerals in Isabelle2011/12/13 -------------";
 
    10 "----------- inst_bdv -----------------------------------";
 
    11 "----------- inst_bdv -----------------------------------";
 
    11 "----------- subst_atomic_all ---------------------------";
 
    12 "----------- subst_atomic_all ---------------------------";
 
    12 "----------- Pattern.match ------------------------------";
 
    13 "----------- Pattern.match ------------------------------";
 
    13 "----------- fun TermC.matches --------------------------------";
 
    14 "----------- fun TermC.matches --------------------------------";
 
    32 "----------- fun inst_abs ----------------------------------------------------------------------";
 
    33 "----------- fun inst_abs ----------------------------------------------------------------------";
 
    33 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
 
    34 "----------- fun ThmC_Def.num_to_Free -------------------------------------------------------------";
 
    34 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
 
    35 "----------- fun mk_frac, proper term with uminus ----------------------------------------------";
 
    35 "--------------------------------------------------------";
 
    36 "--------------------------------------------------------";
 
    36 "--------------------------------------------------------";
 
    37 "--------------------------------------------------------";
 
       
    38 
       
    39 "----------- fun is_atom -----------------------------------------------------------------------";
 
       
    40 "----------- fun is_atom -----------------------------------------------------------------------";
 
       
    41 "----------- fun is_atom -----------------------------------------------------------------------";
 
    37 
    42 
    38 "----------- numerals in Isabelle2011/12/13 -------------";
 
    43 "----------- numerals in Isabelle2011/12/13 -------------";
 
    39 "----------- numerals in Isabelle2011/12/13 -------------";
 
    44 "----------- numerals in Isabelle2011/12/13 -------------";
 
    40 "----------- numerals in Isabelle2011/12/13 -------------";
 
    45 "----------- numerals in Isabelle2011/12/13 -------------";
 
    41 "***Isabelle2011 ~= Isabelle2012 = Isabelle2013";
 
    46 "***Isabelle2011 ~= Isabelle2012 = Isabelle2013";
wneuper/isa