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.
Miniscoping rules are deleted, as these brittle proofs
authorpaulson
Thu, 05 Sep 1996 10:29:20 +0200
changeset 1950 97f1c6bf3ace
parent 1949 1badf0b08040
child 1951 f2b8005bdc6e
Miniscoping rules are deleted, as these brittle proofs would otherwise have to be entirely redone
src/HOL/Lex/AutoChopper.ML file | annotate | diff | comparison | revisions
src/HOL/MiniML/W.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lex/AutoChopper.ML	Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Thu Sep 05 10:29:20 1996 +0200
@@ -6,6 +6,8 @@
 Main result: auto_chopper satisfies the is_auto_chopper specification.
 *)
 
+Delsimps (ex_simps @ all_simps);
+
 open AutoChopper;
 
 infix repeat_RS;
--- a/src/HOL/MiniML/W.ML	Thu Sep 05 10:27:36 1996 +0200
+++ b/src/HOL/MiniML/W.ML	Thu Sep 05 10:29:20 1996 +0200
@@ -9,6 +9,7 @@
 open W;
 
 Addsimps [Suc_le_lessD];
+Delsimps (ex_simps @ all_simps);
 
 (* correctness of W with respect to has_type *)
 goal W.thy
isabelle