| changeset 25218 | fcf0f50e478c |
| parent 25217 | 3224db6415ae |
| child 25520 | e123c81257a5 |
--- a/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:32 2007 +0200 +++ b/src/Tools/Compute_Oracle/compute.ML Sat Oct 27 18:37:33 2007 +0200 @@ -35,12 +35,16 @@ val setup_compute : theory -> theory + val print_encoding : bool ref + end structure Compute :> COMPUTE = struct open Report; +val print_encoding = ref false + datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML (* Terms are mapped to integer codes *)