Mercurial Mercurial > hg > nominal2 / 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.
tuned
authorChristian Urban <urbanc@in.tum.de>
Sun, 11 Apr 2010 18:11:23 +0200
changeset 1806 90095f23fc60
parent 1805 f187f20f0a79
child 1807 8a71e90cccd0
tuned
Nominal/Fv.thy file | annotate | diff | comparison | revisions
Nominal/Nominal2_FSet.thy file | annotate | diff | comparison | revisions
Nominal/Parser.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Fv.thy	Sun Apr 11 18:11:13 2010 +0200
+++ b/Nominal/Fv.thy	Sun Apr 11 18:11:23 2010 +0200
@@ -1,5 +1,6 @@
 theory Fv
-imports "../Nominal-General/Nominal2_Atoms" "Abs" "Perm" "Rsp" "Nominal2_FSet"
+imports "../Nominal-General/Nominal2_Atoms" 
+        "Abs" "Perm" "Rsp" "Nominal2_FSet"
 begin
 
 (* The bindings data structure:
--- a/Nominal/Nominal2_FSet.thy	Sun Apr 11 18:11:13 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Sun Apr 11 18:11:23 2010 +0200
@@ -1,5 +1,6 @@
 theory Nominal2_FSet
-imports FSet "../Nominal-General/Nominal2_Supp"
+imports "../Nominal-General/Nominal2_Supp"
+        FSet 
 begin
 
 lemma permute_rsp_fset[quot_respect]:
--- a/Nominal/Parser.thy	Sun Apr 11 18:11:13 2010 +0200
+++ b/Nominal/Parser.thy	Sun Apr 11 18:11:23 2010 +0200
@@ -1,7 +1,8 @@
 theory Parser
 imports "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift"
+        "../Nominal-General/Nominal2_Supp" 
+        "Perm" "Fv" "Rsp" "Lift"
 begin
 
 section{* Interface for nominal_datatype *}
nominal2