Mercurial Mercurial > repos > isabelle / 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.
src/HOL/HOL.ML
changeset 21379 a0561695167a
parent 21150 405ebd7ba881
child 21546 268b6bed0cc8
equal deleted inserted replaced
21378:cedfce6fc725 21379:a0561695167a 
     1 (* legacy ML bindings *)
 
     1 (* legacy ML bindings *)
 
     2 
     2 
     3 val HOL_cs = HOL.claset;
 
     3 val HOL_cs = HOL.claset;
 
     4 val HOL_basic_ss = HOL.simpset_basic;
 
     4 val HOL_basic_ss = HOL.simpset_basic;
 
     5 val HOL_ss = HOL.simpset;
 
     5 val HOL_ss = HOL.simpset;
 
     6 val HOL_css = (HOL.claset, HOL.simpset);
 
       
     7 val hol_simplify = HOL.simplify;
 
     6 val hol_simplify = HOL.simplify;
 
     8 
     7 
     9 val split_tac        = Splitter.split_tac;
 
     8 val split_tac        = Splitter.split_tac;
 
    10 val split_inside_tac = Splitter.split_inside_tac;
 
     9 val split_inside_tac = Splitter.split_inside_tac;
 
    11 val split_asm_tac    = Splitter.split_asm_tac;
 
    10 val split_asm_tac    = Splitter.split_asm_tac;
isabelle