Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Isar_examples/W_correct.thy
changeset 9596 6d6bf351b2cc
parent 9475 b24516d96847
child 9620 1adf6d761c97 
--- a/src/HOL/Isar_examples/W_correct.thy	Mon Aug 14 18:08:26 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Mon Aug 14 18:13:14 2000 +0200
@@ -33,7 +33,7 @@
   "a |- e :: t" == "(a,e,t) : has_type";
 
 inductive has_type
-  intrs [simp]
+  intros [simp]
     Var: "n < length a ==> a |- Var n :: a ! n"
     Abs: "t1#a |- e :: t2 ==> a |- Abs e :: t1 -> t2"
     App: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |]
isabelle