20051029 
urbanc 
20051029 
1) have adjusted the swapping of the result type
in add_datatype_i
2) have replaced map_nth_elem by Library.nth_map
(there seems to be a clash with an existing
nth_map somewhere  therefore the "Library")

file  diff  annotate 
20051028 
urbanc 
20051028 
fixed case names in the weak induction principle and
changed name from "induct" to "induct_weak"

file  diff  annotate 
20051028 
berghofe 
20051028 
Implemented proof of weak induction theorem.

file  diff  annotate 
20051028 
berghofe 
20051028 
Removed legacy prove_goalw_cterm command.

file  diff  annotate 
20051017 
berghofe 
20051017 
Improved proof of injectivity theorems to make it work on
"ordinary" function types as well.

file  diff  annotate 
20051017 
berghofe 
20051017 
Fixed bug in proof of support theorem (it failed on constructors with no arguments).

file  diff  annotate 
20051017 
berghofe 
20051017 
Implemented proofs for support and freshness theorems.

file  diff  annotate 
20051017 
berghofe 
20051017 
Initial revision.

file  diff  annotate 