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.
Modified def.
authornipkow
Sat, 28 Feb 1998 15:41:50 +0100
changeset 4670 f309259fa828
parent 4669 06f3c56dcba8
child 4671 c45cdc1b5e09
Modified def.
src/HOL/Lex/Auto.ML file | annotate | diff | comparison | revisions
src/HOL/Lex/Auto.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lex/Auto.ML	Sat Feb 28 15:41:17 1998 +0100
+++ b/src/HOL/Lex/Auto.ML	Sat Feb 28 15:41:50 1998 +0100
@@ -4,8 +4,6 @@
     Copyright   1995 TUM
 *)
 
-open Auto;
-
 goalw Auto.thy [nexts_def] "nexts A st [] = st";
 by (Simp_tac 1);
 qed"nexts_Nil";
--- a/src/HOL/Lex/Auto.thy	Sat Feb 28 15:41:17 1998 +0100
+++ b/src/HOL/Lex/Auto.thy	Sat Feb 28 15:41:50 1998 +0100
@@ -31,7 +31,7 @@
   "nexts(A) == foldl(next(A))"
 
   accepts :: ('a,'b) auto => 'a list => bool
-  "accepts A xs == fin A (nexts A (start A) xs)"
+  "accepts A == (%xs. fin A (nexts A (start A) xs))"
 
   acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
   "acc_prefix A st xs == ? us. us <= xs & us~=[] & fin A (nexts A st us)"
isabelle