print_translation: does not handle _idtdummy;
authorwenzelm
Fri Oct 07 22:59:18 2005 +0200 (2005-10-07)
changeset 1778132bb237158a5
parent 17780 274eaa114c6d
child 17782 b3846df9d643
print_translation: does not handle _idtdummy;
src/CCL/Term.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/Separation.thy
src/HOL/Library/FuncSet.thy
     1.1 --- a/src/CCL/Term.thy	Fri Oct 07 22:59:17 2005 +0200
     1.2 +++ b/src/CCL/Term.thy	Fri Oct 07 22:59:18 2005 +0200
     1.3 @@ -56,6 +56,7 @@
     1.4  ML {*
     1.5  (** Quantifier translations: variable binding **)
     1.6  
     1.7 +(* FIXME does not handle "_idtdummy" *)
     1.8  (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
     1.9  
    1.10  fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
     2.1 --- a/src/HOL/Hoare/Hoare.thy	Fri Oct 07 22:59:17 2005 +0200
     2.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Oct 07 22:59:18 2005 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4    | com_tr t _ = t (* if t is just a Free/Var *)
     2.5  *}
     2.6  
     2.7 -(* triple_tr *)
     2.8 +(* triple_tr *)    (* FIXME does not handle "_idtdummy" *)
     2.9  ML{*
    2.10  local
    2.11  
     3.1 --- a/src/HOL/Hoare/HoareAbort.thy	Fri Oct 07 22:59:17 2005 +0200
     3.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Fri Oct 07 22:59:18 2005 +0200
     3.3 @@ -103,7 +103,7 @@
     3.4    | com_tr t _ = t (* if t is just a Free/Var *)
     3.5  *}
     3.6  
     3.7 -(* triple_tr *)
     3.8 +(* triple_tr *)  (* FIXME does not handle "_idtdummy" *)
     3.9  ML{*
    3.10  local
    3.11  
     4.1 --- a/src/HOL/Hoare/Separation.thy	Fri Oct 07 22:59:17 2005 +0200
     4.2 +++ b/src/HOL/Hoare/Separation.thy	Fri Oct 07 22:59:18 2005 +0200
     4.3 @@ -55,6 +55,7 @@
     4.4   "@star" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "**" 60)
     4.5   "@wand" :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "-*" 60)
     4.6  
     4.7 +(* FIXME does not handle "_idtdummy" *)
     4.8  ML{*
     4.9  (* free_tr takes care of free vars in the scope of sep. logic connectives:
    4.10     they are implicitly applied to the heap *)
     5.1 --- a/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:17 2005 +0200
     5.2 +++ b/src/HOL/Library/FuncSet.thy	Fri Oct 07 22:59:18 2005 +0200
     5.3 @@ -35,7 +35,7 @@
     5.4  
     5.5  translations
     5.6    "PI x:A. B" => "Pi A (%x. B)"
     5.7 -  "A -> B" => "Pi A (_K B)"
     5.8 +  "A -> B" => "Pi A (%_. B)"
     5.9    "%x:A. f" == "restrict (%x. f) A"
    5.10  
    5.11  constdefs