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.
take out Class.thy again, because it does not yet compile cleanly
authorurbanc
Wed, 06 Jun 2007 21:24:35 +0200
changeset 23283 c7ab7051aba0
parent 23282 dfc459989d24
child 23284 07ae93e58fea
take out Class.thy again, because it does not yet compile cleanly
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOL/Nominal/Examples/ROOT.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Wed Jun 06 20:49:04 2007 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 06 21:24:35 2007 +0200
@@ -774,7 +774,7 @@
   Nominal/Examples/ROOT.ML \
   Nominal/Examples/CR.thy \
   Nominal/Examples/CR_Takahashi.thy \
-  Nominal/Examples/Class.thy \
+##  Nominal/Examples/Class.thy \
   Nominal/Examples/Compile.thy \
   Nominal/Examples/Fsub.thy \
   Nominal/Examples/Lambda_mu.thy \
--- a/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 06 20:49:04 2007 +0200
+++ b/src/HOL/Nominal/Examples/ROOT.ML	Wed Jun 06 21:24:35 2007 +0200
@@ -5,7 +5,7 @@
 Various examples involving nominal datatypes.
 *)
 
-use_thy "Class"; 
+(*use_thy "Class";*)
 use_thy "CR";
 use_thy "CR_Takahashi";
 use_thy "Compile";
isabelle