Eps -> Hilbert_Choice.Eps
authorberghofe
Tue May 28 09:46:39 2002 +0200 (2002-05-28)
changeset 1318221851696dbf0
parent 13181 dc393bbee6ce
child 13183 c7290200b3f4
Eps -> Hilbert_Choice.Eps
TFL/dcterm.ML
TFL/usyntax.ML
     1.1 --- a/TFL/dcterm.ML	Mon May 27 17:20:16 2002 +0200
     1.2 +++ b/TFL/dcterm.ML	Tue May 28 09:46:39 2002 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  val dest_disj   = dest_binop "op |"
     1.5  val dest_cons   = dest_binop "Cons"
     1.6  val dest_let    = Library.swap o dest_binop "Let";
     1.7 -val dest_select = dest_binder "Eps"
     1.8 +val dest_select = dest_binder "Hilbert_Choice.Eps"
     1.9  val dest_exists = dest_binder "Ex"
    1.10  val dest_forall = dest_binder "All"
    1.11  
     2.1 --- a/TFL/usyntax.ML	Mon May 27 17:20:16 2002 +0200
     2.2 +++ b/TFL/usyntax.ML	Tue May 28 09:46:39 2002 +0200
     2.3 @@ -167,7 +167,7 @@
     2.4  
     2.5  fun mk_select (r as {Bvar,Body}) =
     2.6    let val ty = type_of Bvar
     2.7 -      val c = Const("Eps",(ty --> HOLogic.boolT) --> ty)
     2.8 +      val c = Const("Hilbert_Choice.Eps",(ty --> HOLogic.boolT) --> ty)
     2.9    in list_comb(c,[mk_abs r])
    2.10    end;
    2.11