# HG changeset patch # User huffman # Date 1333533008 -7200 # Node ID e0bff2ae939faa8c533715b0d299b16fd9fd3cd4 # Parent 0193e663a19e3891895132257cf70eb22267b1f6 fix typos diff -r 0193e663a19e -r e0bff2ae939f src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 13:42:01 2012 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Apr 04 11:50:08 2012 +0200 @@ -1,7 +1,7 @@ (* Title: HOL/Tools/Lifting/lifting_setup.ML Author: Ondrej Kuncar -Setting the lifting infranstructure up. +Setting up the lifting infrastructure. *) signature LIFTING_SETUP = @@ -39,7 +39,7 @@ Const (@{const_name equivp}, _) $ _ => abs_fun_graph | Const (@{const_name part_equivp}, _) $ rel => HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph) - | _ => raise SETUP_LIFTING_INFR "unsopported equivalence theorem" + | _ => raise SETUP_LIFTING_INFR "unsupported equivalence theorem" ) val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body)); val qty_name = (fst o dest_Type) qty @@ -107,7 +107,7 @@ val _ = Outer_Syntax.local_theory @{command_spec "setup_lifting"} - "Setup lifting infrastracture" + "Setup lifting infrastructure" (Parse_Spec.xthm >> (fn xthm => setup_by_typedef_thm_aux xthm)) end;