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

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

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

revision 3567 by xiny, Sun Mar 24 07:54:36 2002 UTC revision 3568 by xiny, Tue Apr 9 05:57:54 2002 UTC
# Line 1  Line 1 
 include Czf_itt_set  
1  include Czf_itt_dall  include Czf_itt_dall
2  include Czf_itt_dexists  include Czf_itt_dexists
3    
# Line 24  Line 23 
23  open Base_dtactic  open Base_dtactic
24  open Base_auto_tactic  open Base_auto_tactic
25    
26  declare set_bvd{'s; x. 'a['x]}  declare set_bvd{'s; x. 'a['x]}             (* { a(x) | x in s } *)
27    declare setbvd_prop{'s; x. 'p['x]}        (* { x in s | p(x) } *)
28    
29  rewrite unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->  rewrite unfold_set_bvd: set_bvd{'s; x. 'a['x]} <-->
30     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}     set_ind{'s; t, f, g. collect{'t; y. 'a['f 'y]}}

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

  ViewVC Help
Powered by ViewVC 1.1.26