branch | decompose-isar |
changeset 41928 | 20138d6136cd |
parent 41926 | 460baed1d047 |
child 41931 | ca6aac81b893 |
1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 15:19:26 2011 +0100 1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Mar 10 16:04:00 2011 +0100 1.3 @@ -33,7 +33,7 @@ 1.4 ML {* 1.5 val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "x::int")]; 1.6 val t = parseNEW ctxt "x + 1 = (2::int)"; 1.7 -*} 1.8 +*} 1.9 1.10 ML {* 1.11 rewrite_inst_ thy e_rew_ord e_rls true subst (@{thm "int_isolate_add"}) t;