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.
Eps -> Hilbert_Choice.Eps
authorberghofe
Tue, 28 May 2002 09:46:39 +0200
changeset 13182 21851696dbf0
parent 13181 dc393bbee6ce
child 13183 c7290200b3f4
Eps -> Hilbert_Choice.Eps
TFL/dcterm.ML file | annotate | diff | comparison | revisions
TFL/usyntax.ML file | annotate | diff | comparison | revisions 
--- a/TFL/dcterm.ML	Mon May 27 17:20:16 2002 +0200
+++ b/TFL/dcterm.ML	Tue May 28 09:46:39 2002 +0200
@@ -136,7 +136,7 @@
 val dest_disj   = dest_binop "op |"
 val dest_cons   = dest_binop "Cons"
 val dest_let    = Library.swap o dest_binop "Let";
-val dest_select = dest_binder "Eps"
+val dest_select = dest_binder "Hilbert_Choice.Eps"
 val dest_exists = dest_binder "Ex"
 val dest_forall = dest_binder "All"
 
--- a/TFL/usyntax.ML	Mon May 27 17:20:16 2002 +0200
+++ b/TFL/usyntax.ML	Tue May 28 09:46:39 2002 +0200
@@ -167,7 +167,7 @@
 
 fun mk_select (r as {Bvar,Body}) =
   let val ty = type_of Bvar
-      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
+      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
   in list_comb(c,[mk_abs r])
   end;
isabelle