menu

Return to entry

ML_Args_Antiquotations
Gen_ML_Typeclasses_Base
ML_Eval_Antiquotation
ML_Typeclasses_Base
ML_Bi_Typeclasses
ML_Categories
ML_Coroutines
ML_ITypeclasses_Base
ML_ICategories
ML_Lenses
ML_State_Base
ML_State
ML_Typeclasses
ML_ITypeclasses
Extended_Metis_Data
Zippy_ML_Tactic_Utils
Cases_Tactics
Cases_Tactics_HOL
Extended_Blast_Data
Generic_Term_Index_Data
ML_Priority_Queues
Zippy_Actions_Base
Zippy_Base_Setup
ML_IMap_Antiquotation
ML_Gen_Zippers_Base
ML_Gen_Zippers_Setup
ML_Morphs
ML_Structured_Lenses
ML_Zippers
ML_Linked_Zippers
ML_Alternating_Zippers
ML_Zipper_Utils
ML_Alternating_Zipper_Utils
Zippy_Exceptions
Zippy_Loggers
Zippy_Shows
Zippy_States
Zippy_Base
Zippy_Coroutines
Zippy_Enums
Zippy_Identifiers
Zippy_Actions
ML_Alternating_Zipper_Nodes
ML_Zipper_Directions
ML_Zipper_Positions
ML_Lists
ML_Zipper_Instances
ML_Alternating_Zipper_Instances
ML_Zipper_Position_Utils
ML_Alternating_Zipper_Paths
Zippy_Nodes
Zippy_Positions
Zippy_Actions_Positions
ML_Union_Find
Zippy_Goals_Base
Zippy_Goals
Zippy_Lists_Base
Zippy_Lists_Goals
Generic_Table_Data
Zippy_Action_Clusters
Zippy_Goal_Pos_Updates_Base
Zippy_Goal_Pos_Updates
Zippy_Lists_Goal_Pos_Updates
Zippy_Collect
Zippy_Lists_Collect
Zippy_Lists_Positions
Zippy_Lists_Positions_Collect
Zippy_Action_Applications_Base
Zippy_Action_Applications
Zippy_Tactics_Base
Zippy_Tactics
Zippy_Instance
Zippy_Instance_Hom_Changed_Goals_Data
Zippy_Instance_Cases
Zippy_Instance_Classical
Induction_Tactics
Zippy_Instance_Induction
Zippy_Instance_Subst
Context_Parsers
Extended_Simp_Data
Zippy_Instance_Resolve
Zippy_Instance_Resolves_Simp
Zippy_Runs_Base
Zippy_Seqs
Zippy_Runs
Zippy_Instance_Pure
Zippy_Instance_Simp
Zip_Pure
Zip_HOL
Zip_Metis
Zip_Try0
Zip_Examples
Zippy_Paper

Zippy.Zippy_Instance_Induction

HTML Presentation