20051125 
urbanc 
20051125 
added fsub.thy (poplmark challenge) to the examples
directory.

file  diff  annotate 
20051125 
berghofe 
20051125 
Fixed problem with strong induction theorem for datatypes containing
no atom types (ind_sort was the empty sort in this case).

file  diff  annotate 
20051110 
urbanc 
20051110 
called the induction principle "unsafe" instead of "test".

file  diff  annotate 
20051107 
berghofe 
20051107 
Added strong induction theorem (currently only axiomatized!).

file  diff  annotate 
20051107 
urbanc 
20051107 
added thms perm, distinct and fresh to the simplifier.
One would liket to add also inject, but this causes
problems with "congruences" like
Lam [a].t1 = Lam [b].t2
P (Lam [a].t1)

P (Lam [b].t2)
because the equation "Lam [a].t1 = Lam [b].t2" would simplify
to "[a].t1 = [b].t2" and then the goal is not true just by
simplification.

file  diff  annotate 
20051102 
berghofe 
20051102 
Moved atom stuff to new file nominal_atoms.ML

file  diff  annotate 
20051102 
urbanc 
20051102 
 completed the list of thms for supp_atm
 cleaned up the way how thms are collected under single names

file  diff  annotate 
20051102 
berghofe 
20051102 
Added code for proving that new datatype has finite support.

file  diff  annotate 
20051102 
urbanc 
20051102 
added the collection of lemmas "supp_at"

file  diff  annotate 
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 