/[mojave]/metaprl/theories/czf/czf_itt_inv_image.mli
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_inv_image.mli

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3566 by xiny, Sun Mar 24 08:21:13 2002 UTC revision 3567 by xiny, Tue Apr 9 05:57:26 2002 UTC
# Line 1  Line 1 
1  include Czf_itt_set  include Czf_itt_set
2  include Czf_itt_member  include Czf_itt_set_bvd
3    
4  open Printf  open Printf
5  open Mp_debug  open Mp_debug
# Line 24  Line 24 
24  open Base_auto_tactic  open Base_auto_tactic
25    
26  declare inv_image{'s; x. 'a['x]; 't}  (* { x in s | a(x) in t } *)  declare inv_image{'s; x. 'a['x]; 't}  (* { x in s | a(x) in t } *)
27    
28    rewrite unfold_inv_image: inv_image{'s; x. 'a['x]; 't} <-->
29       setbvd_prop{'s; x. mem{'a['x]; 't}}
30    
31    topval fold_inv_image : conv

Legend:
Removed from v.3566  
changed lines
  Added in v.3567

  ViewVC Help
Powered by ViewVC 1.1.26