src/Pure/thm.ML
changeset 10486 7b07dd104a1a
parent 10416 5b33e732e459
child 10767 8fa4aafa7314
equal deleted inserted replaced
10485:f1576723371f 10486:7b07dd104a1a
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     4     Copyright   1994  University of Cambridge
     5 
     5 
     6 The core of Isabelle's Meta Logic: certified types and terms, meta
     6 The core of Isabelle's Meta Logic: certified types and terms, meta
     7 theorems, meta rules (including resolution and simplification).
     7 theorems, meta rules (including lifting and resolution).
     8 *)
     8 *)
     9 
     9 
    10 signature BASIC_THM =
    10 signature BASIC_THM =
    11   sig
    11   sig
    12   (*certified types*)
    12   (*certified types*)
   860     {sign_ref = sign_ref,  
   860     {sign_ref = sign_ref,  
   861      der = infer_derivs (Beta_conversion ct, []),
   861      der = infer_derivs (Beta_conversion ct, []),
   862      maxidx = maxidx,
   862      maxidx = maxidx,
   863      shyps = add_term_sorts (t, []),
   863      shyps = add_term_sorts (t, []),
   864      hyps = [],
   864      hyps = [],
   865      prop = Logic.mk_equals (t, if full then Envir.norm_term (Envir.empty 0) t
   865      prop = Logic.mk_equals (t, if full then Envir.beta_norm t
   866        else case t of
   866        else case t of
   867           Abs(_, _, bodt) $ u => subst_bound (u, bodt)
   867           Abs(_, _, bodt) $ u => subst_bound (u, bodt)
   868         | _ => raise THM ("beta_conversion: not a redex", 0, []))}
   868         | _ => raise THM ("beta_conversion: not a redex", 0, []))}
   869   end;
   869   end;
   870 
   870