1.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 13:42:01 2012 +0200
1.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 11:50:08 2012 +0200
1.3 @@ -1,7 +1,7 @@
1.4 (* Title: HOL/Tools/Lifting/lifting_setup.ML
1.5 Author: Ondrej Kuncar
1.6
1.7 -Setting the lifting infranstructure up.
1.8 +Setting up the lifting infrastructure.
1.9 *)
1.10
1.11 signature LIFTING_SETUP =
1.12 @@ -39,7 +39,7 @@
1.13 Const (@{const_name equivp}, _) $ _ => abs_fun_graph
1.14 | Const (@{const_name part_equivp}, _) $ rel =>
1.15 HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
1.16 - | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem"
1.17 + | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem"
1.18 )
1.19 val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
1.20 val qty_name = (fst o dest_Type) qty
1.21 @@ -107,7 +107,7 @@
1.22
1.23 val _ =
1.24 Outer_Syntax.local_theory @{command_spec "setup_lifting"}
1.25 - "Setup lifting infrastracture"
1.26 + "Setup lifting infrastructure"
1.27 (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm))
1.28
1.29 end;