doc-src/IsarRef/Thy/ROOT-ZF.ML
author wenzelm
Fri, 26 Feb 2010 23:08:45 +0100
changeset 35392 5da5ac6c6b77
parent 32833 f3716d1a2e48
child 37216 3165bc303f66
permissions -rw-r--r--
gen_dest_case: recovered @{const_name} from c8a6fae0ad0c, because of separate Syntax.mark_const in case_tr' -- avoid extra syntax markers in output;

Unsynchronized.set ThyOutput.source;
use "../../antiquote_setup.ML";

use_thy "ZF_Specific";