Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed header to cope with default if_weak_cong
authorpaulson
Thu, 08 Jul 1999 13:46:29 +0200
changeset 6919 7985b229806c
parent 6918 63c9df6b5c4b
child 6920 c912740c3545
changed header to cope with default if_weak_cong
src/HOL/TLA/Memory/MemoryImplementation.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Thu Jul 08 13:44:47 1999 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Thu Jul 08 13:46:29 1999 +0200
@@ -15,6 +15,8 @@
 
 (* --------------------------- automatic prover --------------------------- *)
 
+Delcongs [if_weak_cong];
+
 val MI_css = (claset(), simpset());
 
 (* A more aggressive variant that tries to solve subgoals by assumption
isabelle