equal
deleted
inserted
replaced
43 instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) |
43 instance nat :: ml_equiv .. (* Attention: This conflicts with the "EfficientNat" theory *) |
44 instance bool :: ml_equiv .. |
44 instance bool :: ml_equiv .. |
45 instance list :: (ml_equiv) ml_equiv .. |
45 instance list :: (ml_equiv) ml_equiv .. |
46 |
46 |
47 ML {* |
47 ML {* |
48 structure Eval_Method = Proof_Data ( |
48 structure Eval_Method = Proof_Data |
|
49 ( |
49 type T = unit -> bool |
50 type T = unit -> bool |
|
51 (* FIXME avoid user error with non-user text *) |
50 fun init _ () = error "Eval_Method" |
52 fun init _ () = error "Eval_Method" |
51 ) |
53 ) |
52 *} |
54 *} |
53 |
55 |
54 oracle eval_witness_oracle = {* fn (cgoal, ws) => |
56 oracle eval_witness_oracle = {* fn (cgoal, ws) => |