1 theory AbsRepTest

     1 theory AbsRepTest

     2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List

     2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List

     3 begin

     3 begin

     4 

     4 

     5 ML_command "ProofContext.debug := false"

     7 ML_command "ProofContext.debug := false"

     6 ML_command "ProofContext.verbose := false"

     8 ML_command "ProofContext.verbose := false"

     7 

    10 

     8 ML {*

    11 ML {*

     9 val ctxt0 = @{context}

    12 val ctxt0 = @{context}

    10 val ty = Syntax.read_typ ctxt0 "bool"  

    13 val ty = Syntax.read_typ ctxt0 "bool"  

    11 val ctxt1 = Variable.declare_typ ty ctxt0 

    14 val ctxt1 = Variable.declare_typ ty ctxt0