Quot/Examples/AbsRepTest.thy
changeset 831 224909b9399f
parent 824 cedfe2a71298
child 852 67e5da3a356a
equal deleted inserted replaced
830:89d772dae4d4 831:224909b9399f
     8 fun test_funs flag ctxt (rty, qty) =
     8 fun test_funs flag ctxt (rty, qty) =
     9   (absrep_fun_chk flag ctxt (rty, qty)
     9   (absrep_fun_chk flag ctxt (rty, qty)
    10    |> Syntax.string_of_term ctxt
    10    |> Syntax.string_of_term ctxt
    11    |> writeln;
    11    |> writeln;
    12    equiv_relation_chk ctxt (rty, qty) 
    12    equiv_relation_chk ctxt (rty, qty) 
    13    |> Syntax.string_of_term ctxt
       
    14    |> writeln;
       
    15    new_equiv_relation_chk ctxt (rty, qty) 
       
    16    |> Syntax.string_of_term ctxt
    13    |> Syntax.string_of_term ctxt
    17    |> writeln)
    14    |> writeln)
    18 *}
    15 *}
    19 
    16 
    20 definition
    17 definition