1 theory Advanced

     2 imports Essential

     3 begin

     4 

     5 lemma "True"

     6 proof -

     7   ML_prf {* Variable.dest_fixes @{context} *}

     8   fix x y

     9   ML_prf {* Variable.dest_fixes @{context} *}

    10   show ?thesis by auto

    11 qed

    12 

    13 lemma "True"

    14 proof -

    15   fix x y

    16   { fix z w

    17     ML_prf {* Variable.dest_fixes @{context} *}

    18   }

    19   ML_prf {* Variable.dest_fixes @{context} *}

    20   show ?thesis by auto

    21 qed

    22 

    23 ML {*

    24 val ctxt0 = @{context};

    25 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;

    26 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1;

    27 val trm = @{term "(x, y, z, w)"};

    28 

    29   pwriteln (Pretty.chunks

    30     [ pretty_term ctxt0 trm,

    31       pretty_term ctxt1 trm,

    32       pretty_term ctxt2 trm ])

    33 *}

    34 

    35 ML {*

    36   let

    37      val ctxt0 = @{context}

    38      val (y, ctxt1) = Variable.add_fixes ["x"] ctxt0

    39      val frees = replicate 2 ("x", @{typ nat})

    40   in

    41      (Variable.variant_frees ctxt0 [] frees,

    42       Variable.variant_frees ctxt1 [] frees, y)

    43   end

    44 *}

    45 

    46 end