diff --git a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
index 7c66fc1c23..61ae8f7b6c 100644
--- a/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Isabelle/Translation/FromTyped.hs
@@ -56,7 +56,9 @@ goModule onlyTypes infoTable Internal.Module {..} =
   Theory
     { _theoryName = over nameText toIsabelleName $ over namePretty toIsabelleName _moduleName,
       _theoryImports = map (^. Internal.importModuleName) (_moduleBody ^. Internal.moduleImports),
-      _theoryStatements = concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
+      _theoryStatements = case _modulePragmas ^. pragmasIsabelleIgnore of
+        Just (PragmaIsabelleIgnore True) -> []
+        _ -> concatMap goMutualBlock (_moduleBody ^. Internal.moduleStatements)
     }
   where
     toIsabelleName :: Text -> Text
@@ -75,13 +77,18 @@ goModule onlyTypes infoTable Internal.Module {..} =
     goMutualBlock :: Internal.MutualBlock -> [Statement]
     goMutualBlock Internal.MutualBlock {..} =
       filter (\stmt -> not onlyTypes || isTypeDef stmt) $
-        map goMutualStatement (toList _mutualStatements)
+        mapMaybe goMutualStatement (toList _mutualStatements)
 
-    goMutualStatement :: Internal.MutualStatement -> Statement
+    checkNotIgnored :: Pragmas -> a -> Maybe a
+    checkNotIgnored pragmas x = case pragmas ^. pragmasIsabelleIgnore of
+      Just (PragmaIsabelleIgnore True) -> Nothing
+      _ -> Just x
+
+    goMutualStatement :: Internal.MutualStatement -> Maybe Statement
     goMutualStatement = \case
-      Internal.StatementInductive x -> goInductiveDef x
-      Internal.StatementFunction x -> goFunctionDef x
-      Internal.StatementAxiom x -> goAxiomDef x
+      Internal.StatementInductive x -> checkNotIgnored (x ^. Internal.inductivePragmas) $ goInductiveDef x
+      Internal.StatementFunction x -> checkNotIgnored (x ^. Internal.funDefPragmas) $ goFunctionDef x
+      Internal.StatementAxiom x -> checkNotIgnored (x ^. Internal.axiomPragmas) $ goAxiomDef x
 
     goInductiveDef :: Internal.InductiveDef -> Statement
     goInductiveDef Internal.InductiveDef {..}
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 7cbcdb536f..7e52ff866e 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
@@ -1650,7 +1650,7 @@ checkSections sec = topBindings helper
                                   _projectionKind = kind,
                                   _projectionFieldBuiltin = field ^. fieldBuiltin,
                                   _projectionDoc = field ^. fieldDoc,
-                                  _projectionPragmas = field ^. fieldPragmas
+                                  _projectionPragmas = combinePragmas (i ^. inductivePragmas) (field ^. fieldPragmas)
                                 }
                               where
                                 kind :: ProjectionKind
@@ -1658,6 +1658,19 @@ checkSections sec = topBindings helper
                                   ExplicitField -> ProjectionExplicit
                                   ImplicitInstanceField -> ProjectionCoercion
 
+                                combinePragmas :: Maybe ParsedPragmas -> Maybe ParsedPragmas -> Maybe ParsedPragmas
+                                combinePragmas p1 p2 = case (p1, p2) of
+                                  (Nothing, Nothing) -> Nothing
+                                  (Just p, Nothing) -> Just p
+                                  (Nothing, Just p) -> Just p
+                                  (Just p1', Just p2') ->
+                                    Just
+                                      ( over
+                                          (withLocParam . withSourceValue . pragmasIsabelleIgnore)
+                                          (\i2 -> i2 <|> (p1' ^. withLocParam . withSourceValue . pragmasIsabelleIgnore))
+                                          p2'
+                                      )
+
                             getFields :: Sem (Fail ': s') [RecordStatement 'Parsed]
                             getFields = case i ^. inductiveConstructors of
                               c :| [] -> case c ^. constructorRhs of
diff --git a/src/Juvix/Data/Pragmas.hs b/src/Juvix/Data/Pragmas.hs
index ad0690e065..641692887e 100644
--- a/src/Juvix/Data/Pragmas.hs
+++ b/src/Juvix/Data/Pragmas.hs
@@ -71,6 +71,11 @@ newtype PragmaIsabelleFunction = PragmaIsabelleFunction
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
+newtype PragmaIsabelleIgnore = PragmaIsabelleIgnore
+  { _pragmaIsabelleIgnore :: Bool
+  }
+  deriving stock (Show, Eq, Ord, Data, Generic)
+
 data Pragmas = Pragmas
   { _pragmasInline :: Maybe PragmaInline,
     _pragmasUnroll :: Maybe PragmaUnroll,
@@ -82,7 +87,8 @@ data Pragmas = Pragmas
     _pragmasSpecialiseBy :: Maybe PragmaSpecialiseBy,
     _pragmasEval :: Maybe PragmaEval,
     _pragmasIsabelleOperator :: Maybe PragmaIsabelleOperator,
-    _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction
+    _pragmasIsabelleFunction :: Maybe PragmaIsabelleFunction,
+    _pragmasIsabelleIgnore :: Maybe PragmaIsabelleIgnore
   }
   deriving stock (Show, Eq, Ord, Data, Generic)
 
@@ -121,6 +127,8 @@ instance Hashable PragmaIsabelleOperator
 
 instance Hashable PragmaIsabelleFunction
 
+instance Hashable PragmaIsabelleIgnore
+
 instance Hashable Pragmas
 
 instance Serialize PragmaInline
@@ -171,6 +179,10 @@ instance Serialize PragmaIsabelleFunction
 
 instance NFData PragmaIsabelleFunction
 
+instance Serialize PragmaIsabelleIgnore
+
+instance NFData PragmaIsabelleIgnore
+
 instance Serialize Pragmas
 
 instance NFData Pragmas
@@ -201,6 +213,7 @@ instance FromJSON Pragmas where
         _pragmasEval <- keyMay "eval" parseEval
         _pragmasIsabelleOperator <- keyMay "isabelle-operator" parseIsabelleOperator
         _pragmasIsabelleFunction <- keyMay "isabelle-function" parseIsabelleFunction
+        _pragmasIsabelleIgnore <- keyMay "isabelle-ignore" parseIsabelleIgnore
         return Pragmas {..}
 
       parseInline :: Parse YamlError PragmaInline
@@ -273,6 +286,11 @@ instance FromJSON Pragmas where
         _pragmaIsabelleFunctionName <- key "name" asText
         return PragmaIsabelleFunction {..}
 
+      parseIsabelleIgnore :: Parse YamlError PragmaIsabelleIgnore
+      parseIsabelleIgnore = do
+        _pragmaIsabelleIgnore <- asBool
+        return PragmaIsabelleIgnore {..}
+
       parseSpecialiseArg :: Parse YamlError PragmaSpecialiseArg
       parseSpecialiseArg =
         (SpecialiseArgNum <$> asIntegral)
@@ -316,7 +334,8 @@ instance Semigroup Pragmas where
         _pragmasSpecialiseArgs = p2 ^. pragmasSpecialiseArgs <|> p1 ^. pragmasSpecialiseArgs,
         _pragmasSpecialiseBy = p2 ^. pragmasSpecialiseBy <|> p1 ^. pragmasSpecialiseBy,
         _pragmasIsabelleOperator = p2 ^. pragmasIsabelleOperator,
-        _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction
+        _pragmasIsabelleFunction = p2 ^. pragmasIsabelleFunction,
+        _pragmasIsabelleIgnore = p2 ^. pragmasIsabelleIgnore <|> p1 ^. pragmasIsabelleIgnore
       }
 
 instance Monoid Pragmas where
@@ -332,7 +351,8 @@ instance Monoid Pragmas where
         _pragmasSpecialiseBy = Nothing,
         _pragmasEval = Nothing,
         _pragmasIsabelleOperator = Nothing,
-        _pragmasIsabelleFunction = Nothing
+        _pragmasIsabelleFunction = Nothing,
+        _pragmasIsabelleIgnore = Nothing
       }
 
 adjustPragmaInline :: Int -> PragmaInline -> PragmaInline
diff --git a/tests/positive/Isabelle/Program.juvix b/tests/positive/Isabelle/Program.juvix
index 69d15bdb4e..0cd881bc34 100644
--- a/tests/positive/Isabelle/Program.juvix
+++ b/tests/positive/Isabelle/Program.juvix
@@ -91,6 +91,7 @@ type Either' A B := Left' A | Right' B;
 
 -- Records
 
+{-# isabelle-ignore: true #-}
 type R := mkR {
   r1 : Nat;
   r2 : Nat;
diff --git a/tests/positive/Isabelle/isabelle/Program.thy b/tests/positive/Isabelle/isabelle/Program.thy
index df548c13df..e9c72431aa 100644
--- a/tests/positive/Isabelle/isabelle/Program.thy
+++ b/tests/positive/Isabelle/isabelle/Program.thy
@@ -99,16 +99,6 @@ datatype ('A, 'B) Either'
   = Left' 'A |
     Right' 'B
 
-record R =
-  r1 :: nat
-  r2 :: nat
-
-fun r1 :: "R \<Rightarrow> nat" where
-  "r1 (mkR r1' r2') = r1'"
-
-fun r2 :: "R \<Rightarrow> nat" where
-  "r2 (mkR r1' r2') = r2'"
-
 fun bf :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
   "bf b1 b2 = (\<not> (b1 \<and> b2))"