src/HOL/Bali/Basis.thy
changeset 16417 9bc16273c2d4
parent 16121 a80aa66d2271
child 17785 8d928051d6a7
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     3     Author:     David von Oheimb
     3     Author:     David von Oheimb
     4 
     4 
     5 *)
     5 *)
     6 header {* Definitions extending HOL as logical basis of Bali *}
     6 header {* Definitions extending HOL as logical basis of Bali *}
     7 
     7 
     8 theory Basis = Main:
     8 theory Basis imports Main begin
     9 
     9 
    10 ML {*
    10 ML {*
    11 Unify.search_bound := 40;
    11 Unify.search_bound := 40;
    12 Unify.trace_bound  := 40;
    12 Unify.trace_bound  := 40;
    13 *}
    13 *}