less pervasive names;
authorwenzelm
Sat Oct 17 17:18:59 2009 +0200 (2009-10-17)
changeset 3297155ba9b6648ef
parent 32970 fbd2bb2489a8
child 32972 45ba8b02e1e4
less pervasive names;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sat Oct 17 16:58:03 2009 +0200
     1.2 +++ b/src/Pure/tactic.ML	Sat Oct 17 17:18:59 2009 +0200
     1.3 @@ -46,7 +46,6 @@
     1.4      int -> tactic
     1.5    val net_biresolve_tac: (bool * thm) list -> int -> tactic
     1.6    val net_bimatch_tac: (bool * thm) list -> int -> tactic
     1.7 -  val build_net: thm list -> (int * thm) Net.net
     1.8    val filt_resolve_tac: thm list -> int -> int -> tactic
     1.9    val resolve_from_net_tac: (int * thm) Net.net -> int -> tactic
    1.10    val match_from_net_tac: (int * thm) Net.net -> int -> tactic
    1.11 @@ -75,6 +74,7 @@
    1.12      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    1.13        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.14    val eq_kbrl: ('a * (bool * thm)) * ('a * (bool * thm)) -> bool
    1.15 +  val build_net: thm list -> (int * thm) Net.net
    1.16  end;
    1.17  
    1.18  structure Tactic: TACTIC =
    1.19 @@ -385,5 +385,5 @@
    1.20  
    1.21  end;
    1.22  
    1.23 -structure BasicTactic: BASIC_TACTIC = Tactic;
    1.24 -open BasicTactic;
    1.25 +structure Basic_Tactic: BASIC_TACTIC = Tactic;
    1.26 +open Basic_Tactic;