# 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;