20060906 
haftmann 
20060906 
TypedefPackage.add_typedef_* now yields name of introduced type constructor

file  diff  annotate 
20060824 
berghofe 
20060824 
Added premises concerning finite support of recursion results to FCBs.

file  diff  annotate 
20060818 
berghofe 
20060818 
 Fixed bug that caused uniqueness proof for recursion
combinator to fail for mutually recursive datatypes
 Implemented proofs of characteristic equations for
recursion combinator.

file  diff  annotate 
20060814 
berghofe 
20060814 
Finished implementation of uniqueness proof for recursion combinator.

file  diff  annotate 
20060731 
berghofe 
20060731 
Additional freshness constraints for FCB.

file  diff  annotate 
20060721 
haftmann 
20060721 
adaption to argument change in primrec_package

file  diff  annotate 
20060718 
berghofe 
20060718 
Started implementing uniqueness proof for recursion
combinator (still unfinished).

file  diff  annotate 
20060711 
wenzelm 
20060711 
replaced Term.variant(list) by Name.variant(_list);

file  diff  annotate 
20060708 
wenzelm 
20060708 
Goal.prove_global;

file  diff  annotate 
20060704 
berghofe 
20060704 
Implemented proofs of equivariance and finite support
for graph of recursion combinator.

file  diff  annotate 
20060613 
wenzelm 
20060613 
ProjectRule now context dependent;

file  diff  annotate 
20060612 
berghofe 
20060612 
Completely rewrote code for defining graph of recursion combinator.

file  diff  annotate 
20060609 
berghofe 
20060609 
 Changed naming scheme: names of "internal" constructors now have
"_Rep" as suffix  no need to set unique_names to false any longer
 Cleaned up a bit (removed occurrences of strip_option and replace_types')

file  diff  annotate 
20060524 
berghofe 
20060524 
Extended strong induction rule with additional
freshness constraints.

file  diff  annotate 
20060516 
wenzelm 
20060516 
Sign.certify_sort;

file  diff  annotate 
20060513 
wenzelm 
20060513 
unchecked definitions;

file  diff  annotate 
20060428 
berghofe 
20060428 
Renamed "nominal" theory to "Nominal".

file  diff  annotate 
20060427 
berghofe 
20060427 
SplitAt > chop

file  diff  annotate 
20060410 
berghofe 
20060410 
Adapted to changed type of add_typedef_i.

file  diff  annotate 
20060323 
berghofe 
20060323 
Replaced iteration combinator by recursion combinator.

file  diff  annotate 
20060315 
berghofe 
20060315 
add_inst_arity_i renamed to prove_arity.

file  diff  annotate 
20060313 
berghofe 
20060313 
First version of function for defining graph of iteration combinator.

file  diff  annotate 
20060224 
berghofe 
20060224 
Reverted to old interface of AxClass.add_inst_arity(_i)

file  diff  annotate 
20060224 
berghofe 
20060224 
Adapted to Florian's recent changes to the AxClass package.

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