fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant
(*show_question_marks := false;*)+ −
quick_and_dirty := true;+ −
+ −
no_document use_thy "~~/src/HOL/Library/LaTeXsugar";+ −
+ −
use_thy "Slides6"+ −