equal
deleted
inserted
replaced
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 |