| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Pure/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle ML_Bootstrap.thySprache: Isabelle |
|||||||||||||||
|
(* Title: Pure/ML_Bootstrap.thy Author: Makarius ML bootstrap environment -- with access to low-level structures! *) theory ML_Bootstrap imports Pure begin ML ‹ #allStruct ML_Name_Space.global () |> List.app (fn (name, _) => if member (op =) ML_Name_Space.hidden_structures name then ML (Input.string ("structure " ^ name ^ " = " ^ name)) else ()); structure Output_Primitives = Output_Primitives_Virtual; structure Thread_Data = Thread_Data_Virtual; structure PolyML = PolyML; fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = (); Proofterm.proofs := 0; Context.setmp_generic_context NONE ML ‹ List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures; structure PolyML = struct val pointerEq = pointer_eq; structure IntInf = PolyML.IntInf; datatype context = datatype PolyML.context; datatype pretty = datatype PolyML.pretty; end; › › setup ‹Context.theory_map ML_Env.bootstrap_name_space› declare [[ML_read_global = false, ML_catch_all = true]] end
¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26