Mercurial Mercurial > repos > isabelle / diff
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/Statespace/state_space.ML
changeset 30510 4120fc59dd85
parent 30473 e0b66c11e7e4
child 31723 f5cafe803b55 
--- a/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -149,7 +149,7 @@
    thy
    |> Expression.sublocale_cmd name expr
    |> Proof.global_terminal_proof
-         (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
+         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
    |> ProofContext.theory_of
 
 fun add_locale name expr elems thy =
isabelle