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

Log of /metaprl/theories/czf/czf_itt_inv_image.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 3591 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 28 19:51:58 2002 UTC (19 years, 1 month ago) by nogin
File length: 2467 byte(s)
Diff to previous 3567
- Added an option to be have "THEORIES=all" in mk/config
(instead of THEORIES="long list of theories").
I will change all my nightly scripts to use THEORIES=all.

- Added mc to the default list of TEXTHEORIES. Added a file all-bodies.tex
that would automatically contain \inputs corresponding to TEXTHEORIES.
(Before this change we had to update all-theories.tex by hands whenever TEXTHEORIES
was changed).

- Minor fixes in some display forms.

- Removed theories/caml that never had anything useful.

- Removed a few files from theories/ocaml_doc that seemed to be there by accident
(Jason, can you confirm?).


Revision 3567 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 05:57:26 2002 UTC (19 years, 2 months ago) by xiny
File length: 2470 byte(s)
Diff to previous 3546
1. Redefined inverse image. Previously it was defined by introduction
   and elimination rules; now it can be rewritten with "setbvd_prop".
   Actually, after "setbvd_prop" is defined, the "inv_image" is somewhat
   unnecessary. I keep it here just in case that people may want to use
   the concept of inverse image sometimes.
2. Fixed the error in the previous member elimination rule.


Revision 3546 - (view) (download) (annotate) - [select for diffs]
Added Sun Mar 24 08:21:13 2002 UTC (19 years, 3 months ago) by xiny
File length: 2330 byte(s)
Added the module for the inverse image of set t in set s under function f:
   { x in s | f(x) in t }

I didn't find a direct way to define it, so I define it using axioms.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26