Index of Isabelle/HOL/HOL-Algebra/BPL

Theories

The files have been tested with the Isabelle 2007 distribution. Files from HomGroupCompletion to Basic_Perturbation_Lemma_local_nilpot give the proof of the Basic Perturbation Lemma, on which the code generation experiments are based. They have been built upon the Isabelle implementation of higher-order logic (HOL), making use of the Algebra library (available from http://isabelle.in.tum.de/dist/library/HOL/HOL-Algebra/index.html)

The file "Infinite_Set" is taken from the Isabelle distribution, and is due to Stephan Merz.

• HomGroupCompletion
• HomGroupsCompletion
• lemma_2_2_11
• lemma_2_2_14
• Infinite_Set
• analytic_part_local
• lemma_2_2_15_local_nilpot
• lemma_2_2_17_local_nilpot
• lemma_2_2_18_local_nilpot
• lemma_2_2_19_local_nilpot
• Basic_Perturbation_Lemma_local_nilpot

  In the following file it can be found a compressed version of the previous source files in original ".thy" format

• BPL