author blanchet
Fri Apr 30 09:36:45 2010 +0200 (2010-04-30)
changeset 36569 3a29eb7606c3
parent 33191 fe3c65d9c577
child 36926 90bb12cf8e36
permissions -rw-r--r--
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
     1 Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main