Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified imports;
authorwenzelm
Fri, 21 Apr 2017 16:12:11 +0200
changeset 65535 1bf7b5dc34c8
parent 65534 b6250ee6ce79
child 65536 23c2450ae027
clarified imports;
src/HOL/Proofs/Lambda/WeakNorm.thy file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 21 15:26:24 2017 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Apr 21 16:12:11 2017 +0200
@@ -6,8 +6,7 @@
 section \<open>Weak normalization for simply-typed lambda calculus\<close>
 
 theory WeakNorm
-imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
-  "~~/src/HOL/Library/Code_Target_Int"
+imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int"
 begin
 
 text \<open>
--- a/src/HOL/ROOT	Fri Apr 21 15:26:24 2017 +0200
+++ b/src/HOL/ROOT	Fri Apr 21 16:12:11 2017 +0200
@@ -449,8 +449,7 @@
   *}
   options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
-  theories [document = false]
-    "~~/src/HOL/Library/Code_Target_Int"
+  sessions "HOL-Library"
   theories
     Eta
     StrongNorm
isabelle