Slides/ROOT1.ML
author zhangx
Tue, 09 Feb 2016 22:30:43 +0800
changeset 114 81c6ede5cd11
parent 0 110247f9d47e
permissions -rw-r--r--
More refinements in PIPBasics.thy.

(*show_question_marks := false;*)

no_document use_thy "../CpsG"; 
no_document use_thy "../ExtGG"; 
no_document use_thy "~~/src/HOL/Library/LaTeXsugar";
quick_and_dirty := true;
use_thy "Slides1"