20060123 
krauss 
20060123 
Updated to Isabelle 20060123

file  diff  annotate 
20060119 
berghofe 
20060119 
Use generic Simplifier.simp_add attribute instead
of Simplifier.simp_add_global.

file  diff  annotate 
20060111 
berghofe 
20060111 
Implemented proof of (strong) induction rule.

file  diff  annotate 
20060105 
wenzelm 
20060105 
provide projections of induct_weak, induct_unsafe;

file  diff  annotate 
20060105 
urbanc 
20060105 
changed the name of the type "nOption" to "noption".

file  diff  annotate 
20051210 
urbanc 
20051210 
changed the types in accordance with Florian's changes

file  diff  annotate 
20051208 
berghofe 
20051208 
Adapted to new type of PureThy.add_defs_i.

file  diff  annotate 
20051205 
berghofe 
20051205 
Adapted to new type of store_thmss(_atts).

file  diff  annotate 
20051130 
berghofe 
20051130 
Changed order of predicate arguments and quantifiers in strong induction rule.

file  diff  annotate 
20051129 
berghofe 
20051129 
Corrected atom class constraints in strong induction rule.

file  diff  annotate 
20051126 
berghofe 
20051126 
Corrected treatment of nonrecursive abstraction types.

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