src/Pure/IsaMakefile

remove legacy theorem Lim_inner

#
# IsaMakefile for Pure
#

## targets

default: Pure
images: Pure
test: RAW
all: images test
smlnj: all


## global settings

SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log


## Pure

BOOTSTRAP_FILES = 					\
  General/exn.ML					\
  ML-Systems/compiler_polyml-5.2.ML			\
  ML-Systems/compiler_polyml-5.3.ML			\
  ML-Systems/ml_name_space.ML				\
  ML-Systems/ml_pretty.ML				\
  ML-Systems/ml_system.ML				\
  ML-Systems/multithreading.ML				\
  ML-Systems/multithreading_polyml.ML			\
  ML-Systems/overloading_smlnj.ML			\
  ML-Systems/polyml-5.2.1.ML				\
  ML-Systems/polyml.ML					\
  ML-Systems/polyml_common.ML				\
  ML-Systems/pp_dummy.ML				\
  ML-Systems/pp_polyml.ML				\
  ML-Systems/proper_int.ML				\
  ML-Systems/single_assignment.ML			\
  ML-Systems/single_assignment_polyml.ML		\
  ML-Systems/smlnj.ML					\
  ML-Systems/thread_dummy.ML				\
  ML-Systems/universal.ML				\
  ML-Systems/unsynchronized.ML				\
  ML-Systems/use_context.ML

RAW: $(OUT)/RAW

$(OUT)/RAW: $(BOOTSTRAP_FILES)
	@./mk -r


Pure: $(OUT)/Pure

$(OUT)/Pure: $(BOOTSTRAP_FILES)				\
  Concurrent/bash.ML 					\
  Concurrent/bash_sequential.ML				\
  Concurrent/cache.ML					\
  Concurrent/future.ML					\
  Concurrent/lazy.ML					\
  Concurrent/lazy_sequential.ML				\
  Concurrent/mailbox.ML					\
  Concurrent/par_exn.ML					\
  Concurrent/par_list.ML				\
  Concurrent/par_list_sequential.ML			\
  Concurrent/simple_thread.ML				\
  Concurrent/single_assignment.ML			\
  Concurrent/single_assignment_sequential.ML		\
  Concurrent/synchronized.ML				\
  Concurrent/synchronized_sequential.ML			\
  Concurrent/task_queue.ML				\
  Concurrent/time_limit.ML				\
  General/alist.ML					\
  General/antiquote.ML					\
  General/balanced_tree.ML				\
  General/basics.ML					\
  General/binding.ML					\
  General/buffer.ML					\
  General/file.ML					\
  General/graph.ML					\
  General/heap.ML					\
  General/integer.ML					\
  General/linear_set.ML					\
  General/long_name.ML					\
  General/markup.ML					\
  General/name_space.ML					\
  General/ord_list.ML					\
  General/output.ML					\
  General/path.ML					\
  General/position.ML					\
  General/pretty.ML					\
  General/print_mode.ML					\
  General/properties.ML					\
  General/queue.ML					\
  General/same.ML					\
  General/scan.ML					\
  General/secure.ML					\
  General/seq.ML					\
  General/sha1.ML					\
  General/sha1_polyml.ML				\
  General/source.ML					\
  General/stack.ML					\
  General/symbol.ML					\
  General/symbol_pos.ML					\
  General/table.ML					\
  General/timing.ML					\
  General/url.ML					\
  General/xml.ML					\
  General/yxml.ML					\
  Isar/args.ML						\
  Isar/attrib.ML					\
  Isar/auto_bind.ML					\
  Isar/calculation.ML					\
  Isar/class.ML						\
  Isar/class_declaration.ML				\
  Isar/code.ML						\
  Isar/context_rules.ML					\
  Isar/element.ML					\
  Isar/expression.ML					\
  Isar/generic_target.ML				\
  Isar/isar_cmd.ML					\
  Isar/isar_syn.ML					\
  Isar/keyword.ML					\
  Isar/local_defs.ML					\
  Isar/local_theory.ML					\
  Isar/locale.ML					\
  Isar/method.ML					\
  Isar/named_target.ML					\
  Isar/object_logic.ML					\
  Isar/obtain.ML					\
  Isar/outer_syntax.ML					\
  Isar/overloading.ML					\
  Isar/parse.ML						\
  Isar/parse_spec.ML					\
  Isar/proof.ML						\
  Isar/proof_context.ML					\
  Isar/proof_display.ML					\
  Isar/proof_node.ML					\
  Isar/rule_cases.ML					\
  Isar/rule_insts.ML					\
  Isar/runtime.ML					\
  Isar/skip_proof.ML					\
  Isar/spec_rules.ML					\
  Isar/specification.ML					\
  Isar/token.ML						\
  Isar/toplevel.ML					\
  Isar/typedecl.ML					\
  ML/install_pp_polyml-5.3.ML				\
  ML/install_pp_polyml.ML				\
  ML/ml_antiquote.ML					\
  ML/ml_compiler.ML					\
  ML/ml_compiler_polyml-5.3.ML				\
  ML/ml_context.ML					\
  ML/ml_env.ML						\
  ML/ml_lex.ML						\
  ML/ml_parse.ML					\
  ML/ml_syntax.ML					\
  ML/ml_thms.ML						\
  PIDE/document.ML					\
  PIDE/isar_document.ML					\
  Proof/extraction.ML					\
  Proof/proof_checker.ML				\
  Proof/proof_rewrite_rules.ML				\
  Proof/proof_syntax.ML					\
  Proof/reconstruct.ML					\
  ProofGeneral/pgip.ML					\
  ProofGeneral/pgip_input.ML				\
  ProofGeneral/pgip_isabelle.ML				\
  ProofGeneral/pgip_markup.ML				\
  ProofGeneral/pgip_output.ML				\
  ProofGeneral/pgip_parser.ML				\
  ProofGeneral/pgip_tests.ML				\
  ProofGeneral/pgip_types.ML				\
  ProofGeneral/pgml.ML					\
  ProofGeneral/preferences.ML				\
  ProofGeneral/proof_general_emacs.ML			\
  ProofGeneral/proof_general_pgip.ML			\
  Pure.thy						\
  ROOT.ML						\
  Syntax/ast.ML						\
  Syntax/lexicon.ML					\
  Syntax/local_syntax.ML				\
  Syntax/mixfix.ML					\
  Syntax/parser.ML					\
  Syntax/printer.ML					\
  Syntax/simple_syntax.ML				\
  Syntax/syntax.ML					\
  Syntax/syntax_ext.ML					\
  Syntax/syntax_phases.ML				\
  Syntax/syntax_trans.ML				\
  Syntax/term_position.ML				\
  System/invoke_scala.ML				\
  System/isabelle_process.ML				\
  System/isabelle_system.ML				\
  System/isar.ML					\
  System/session.ML					\
  Thy/html.ML						\
  Thy/latex.ML						\
  Thy/present.ML					\
  Thy/rail.ML						\
  Thy/term_style.ML					\
  Thy/thm_deps.ML					\
  Thy/thy_header.ML					\
  Thy/thy_info.ML					\
  Thy/thy_load.ML					\
  Thy/thy_output.ML					\
  Thy/thy_syntax.ML					\
  Tools/find_consts.ML					\
  Tools/find_theorems.ML				\
  Tools/named_thms.ML					\
  Tools/xml_syntax.ML					\
  assumption.ML						\
  axclass.ML						\
  config.ML						\
  conjunction.ML					\
  consts.ML						\
  context.ML						\
  context_position.ML					\
  conv.ML						\
  defs.ML						\
  display.ML						\
  drule.ML						\
  envir.ML						\
  facts.ML						\
  global_theory.ML					\
  goal.ML						\
  goal_display.ML					\
  interpretation.ML					\
  item_net.ML						\
  library.ML						\
  logic.ML						\
  more_thm.ML						\
  morphism.ML						\
  name.ML						\
  net.ML						\
  pattern.ML						\
  primitive_defs.ML					\
  proofterm.ML						\
  pure_setup.ML						\
  pure_thy.ML						\
  raw_simplifier.ML					\
  search.ML						\
  sign.ML						\
  simplifier.ML						\
  sorts.ML						\
  subgoal.ML						\
  tactic.ML						\
  tactical.ML						\
  term.ML						\
  term_ord.ML						\
  term_sharing.ML					\
  term_subst.ML						\
  term_xml.ML						\
  theory.ML						\
  thm.ML						\
  type.ML						\
  type_infer.ML						\
  type_infer_context.ML					\
  unify.ML						\
  variable.ML
	@./mk


## clean

clean:
	@rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz