equal
deleted
inserted
replaced
1 (* Title: Substitutions/subst.ML |
1 (* Title: HOL/Subst/subst.ML |
|
2 ID: $Id$ |
2 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Author: Martin Coen, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
4 |
5 |
5 For subst.thy. |
6 For subst.thy. |
6 *) |
7 *) |
9 |
10 |
10 (***********) |
11 (***********) |
11 |
12 |
12 val subst_defs = [subst_def,comp_def,sdom_def]; |
13 val subst_defs = [subst_def,comp_def,sdom_def]; |
13 |
14 |
14 val raw_subst_ss = utlemmas_ss addsimps al_rews; |
15 val raw_subst_ss = simpset_of "UTLemmas" addsimps al_rews; |
15 |
16 |
16 local fun mk_thm s = prove_goalw Subst.thy subst_defs s |
17 local fun mk_thm s = prove_goalw Subst.thy subst_defs s |
17 (fn _ => [simp_tac raw_subst_ss 1]) |
18 (fn _ => [simp_tac raw_subst_ss 1]) |
18 in val subst_rews = map mk_thm |
19 in val subst_rews = map mk_thm |
19 ["Const(c) <| al = Const(c)", |
20 ["Const(c) <| al = Const(c)", |