specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;
Learning and using Isabelle
tutorial Tutorial on Isabelle/HOL
main What's in Main
isar-overview Tutorial on Isar
locales Tutorial on Locales
classes Tutorial on Type Classes
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
nitpick User's Guide to Nitpick in Isabelle/HOL
sugar LaTeX Sugar for Isabelle documents
Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
Old Manuals (outdated)
intro Old Introduction to Isabelle
ref Old Isabelle Reference Manual
logics Isabelle's Logics: overview and misc logics
logics-HOL Isabelle's Logics: HOL
logics-ZF Isabelle's Logics: FOL and ZF
ind-defs (Co)Inductive Definitions in ZF