src/Pure/ROOT.ML
changeset 403 4c66b1577753
parent 83 de9316670e89
child 607 72fc777dbda0
equal deleted inserted replaced
402:16a8fe4f2250 403:4c66b1577753
    38 use "thm.ML";
    38 use "thm.ML";
    39 use "drule.ML";
    39 use "drule.ML";
    40 use "tctical.ML";
    40 use "tctical.ML";
    41 use "tactic.ML";
    41 use "tactic.ML";
    42 use "goals.ML";
    42 use "goals.ML";
       
    43 use "axclass.ML";
    43 
    44 
    44 (*Will be visible to all object-logics.*)
    45 (*Will be visible to all object-logics.*)
    45 structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
    46 structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
    46 structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
    47 structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
    47 structure Sequence = SequenceFun();
    48 structure Sequence = SequenceFun();
    57 structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
    58 structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
    58 structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
    59 structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
    59                              and Tactical=Tactical and Net=Net);
    60                              and Tactical=Tactical and Net=Net);
    60 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    61 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    61                            and Tactic=Tactic and Pattern=Pattern);
    62                            and Tactic=Tactic and Pattern=Pattern);
    62 open BasicSyntax Thm Drule Tactical Tactic Goals;
    63 structure AxClass = AxClassFun(structure Logic = Logic 
       
    64   and Goals = Goals and Tactic = Tactic);
       
    65 open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
    63 
    66 
    64 structure Pure = struct val thy = pure_thy end;
    67 structure Pure = struct val thy = pure_thy end;
    65 
    68 
    66 use "install_pp.ML";
    69 use "install_pp.ML";
    67 
    70