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/Knowledge/diophanteq.sml
changeset 60509 2e0b7ca391dc
parent 60500 59a3af532717
child 60519 70b30d910fd5
equal deleted inserted replaced
60508:ce09935439b3 60509:2e0b7ca391dc 
    31     | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
 
    31     | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
 
    32 val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
 
    32 val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
 
    33       SOME t' => t'
 
    33       SOME t' => t'
 
    34     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
 
    34     | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
 
    35 
    35 
    36 val SOME (t,_) = rewrite_inst_ ctxt e_rew_ord Rule_Set.empty true subst 
    36 val SOME (t,_) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst 
    37   @{thm "int_isolate_add"} t; UnparseC.term t;
 
    37   @{thm "int_isolate_add"} t; UnparseC.term t;
 
    38 
    38 
    39 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
    39 val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES"))) t; 
    40 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
 
    40 val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; UnparseC.term t;
 
    41 
    41
wneuper/isa