doc-src/Dirs
author wenzelm
Mon, 27 Aug 2012 23:08:39 +0200
changeset 48952 29562708e05c
parent 47333 8204b1023537
permissions -rw-r--r--
deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48952
29562708e05c deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;
wenzelm
parents: 47333
diff changeset
     1
Inductive TutorialI IsarRef Nitpick Sledgehammer